Binding Contexts as Partitionable Multisets in Abella

TL;DR

This paper extends the Abella proof assistant's handling of binding contexts from ordered sequences to partitionable multisets, enabling reasoning about linearity and related properties in formal systems.

Contribution

It introduces a generalized definition of binding contexts in Abella, based on mappings to sequences, and demonstrates how properties can be automatically lifted to this new framework.

Findings

Binding contexts can be modeled as partitionable multisets in Abella.

Properties from ordered sequences can be lifted to multisets and automated.

The approach supports reasoning about linear logic in formal systems.

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.