FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Formalisation of Barendregt's Variable Convention for Generic Structures with Binders

Authors: Ernesto Copello, Nora Szasz and Alvaro Tasistro

Paper Information

Title:Formalisation of Barendregt's Variable Convention for Generic Structures with Binders
Authors:Ernesto Copello, Nora Szasz and Alvaro Tasistro
Proceedings:LFMTP Regular papers
Editors: Giselle Reis and Frédéric Blanqui
Keywords:Formal Metatheory, Generic Binding Structures, Barendregt's Variable Convention
Abstract:

ABSTRACT. We introduce a universe of regular datatypes with variable binding information, for which we define generic formation, elimination, and induction 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.

Pages:16
Talk:Jul 07 14:30 (Session 28G: Formalization)
Paper: