Binding Contexts as Partitionable Multisets in Abella

TL;DR

The paper addresses how to represent and reason about binding contexts in Abella when linear usage of variables is required. It introduces partitionable binding contexts as multisets built via a multiset union and uses permutation-based lifting to transfer established list-based context properties to the generalized setting, including membership, uniqueness, and distributivity lemmas. It extends the framework to context relations and outlines schematic, automated proofs to streamline reasoning about complex context interactions. The approach enables reasoning about linear object languages and supports a two-level logic methodology by providing a robust mechanism to manage and manipulate binding contexts with resources, paving the way for automation and practical applications in formal reasoning tasks.

Abstract

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.