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

Ernesto Copello
(University of Iowa)
Nora Szasz
(Universidad ORT Uruguay)
Álvaro Tasistro
(Universidad ORT Uruguay)

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.

In Frédéric Blanqui and Giselle Reis: Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2018), Oxford, UK, 7th July 2018, Electronic Proceedings in Theoretical Computer Science 274, pp. 11–26.
Published: 3rd July 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: