A novel formalisation of variable control in languages with implicit names based on de Bruijn indices is presented. We design and implement three languages: first, a restricted language with implicit names; then, a restricted calculus with implicit names and explicit substitution, and finally, an extended calculus with implicit names, implicit substitution and resource control. We propose a novel concept of list types, which are used to give a simple and manageable definition of linearity. We develop an implementation in Haskell.

翻译：本文提出了一种基于德布鲁因索引的隐式名称语言中变量控制的新形式化方法。我们设计并实现了三种语言：首先是一种具有隐式名称的限制性语言；随后是一种具有隐式名称和显式代换的限制性演算；最后是一种具有隐式名称、隐式代换和资源控制的扩展演算。我们提出了列表类型的新概念，用于给出简洁且可处理的线性定义。我们在Haskell中开发了相应的实现。