When reasoning about formal objects whose structures involve binding, it is often necessary to analyze expressions relative to a context that associates types, values, and other related attributes with variables that appear free in the expressions. We refer to such associations as binding contexts. Reasoning tasks also require properties such as the shape and uniqueness of associations concerning binding contexts to be made explicit. The Abella proof assistant, which supports a higher-order treatment of syntactic constructs, provides a simple and elegant way to describe such contexts from which their properties can be extracted. This mechanism is based at the outset on viewing binding contexts as ordered sequences of associations. However, when dealing with object systems that embody notions of linearity, it becomes necessary to treat binding contexts more generally as partitionable multisets. We show how to adapt the original Abella encoding to encompass such a generalization. The key idea in this adaptation is to base the definition of a binding context on a mapping to an underlying ordered sequence of associations. We further show that properties that hold with the ordered sequence view can be lifted to the generalized definition of binding contexts and that this lifting can, in fact, be automated. These ideas find use in the extension currently under development of the two-level logic approach of Abella to a setting where linear logic is used as the specification logic.

翻译：当对结构涉及绑定的形式对象进行推理时，通常需要相对于一个上下文来分析表达式，该上下文将类型、值及其他相关属性与表达式中自由出现的变量相关联。我们将此类关联称为绑定上下文。推理任务还需要明确绑定上下文相关的关联形状与唯一性等属性。支持语法结构高阶处理的Abella证明助手，提供了一种简洁优雅的方式来描述此类上下文，并从中提取其属性。该机制最初基于将绑定上下文视为关联的有序序列。然而，当处理体现线性性概念的对象系统时，需要更一般地将绑定上下文视为可分多集。我们展示了如何调整原始的Abella编码以涵盖此类泛化。此调整的关键思想是将绑定上下文的定义基于到基础关联有序序列的映射。我们进一步证明，在有序序列视图下成立的属性可以提升到绑定上下文的泛化定义，且这种提升实际上可实现自动化。这些思想正被应用于Abella双层逻辑方法的扩展中，该扩展将线性逻辑用作规范逻辑，目前处于开发阶段。