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: |