Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders

TL;DR

This paper formalizes Barendregt's Variable Convention within Constructive Type Theory, providing generic tools for reasoning about variable binding, alpha-equivalence, and substitution in lambda calculus and System F, all verified in Agda.

Contribution

It introduces a universe of regular datatypes with binding, generic alpha-equivalence, and derived induction principles, all formalized and verified in Agda.

Findings

Defined generic alpha-equivalence based on name-swapping.

Derived substitution lemmas for alpha-conversion.

Implemented and verified the framework in Agda.

Abstract

We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then define a generic alpha-equivalence relation over the types of the universe based on name-swapping, and derive iteration and induction principles which work modulo alpha-conversion capturing Barendregt's Variable Convention. We instantiate the resulting framework so as to obtain the Lambda Calculus and System F, for which we derive substitution operations and substitution lemmas for alpha-conversion and substitution composition. The whole work is carried out in Constructive Type Theory and machine-checked by the system Agda.