Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory
We formulate principles of induction and recursion for a variant of lambda calculus with bound names where alpha-conversion is based upon name swapping as in nominal abstract syntax. The principles allow to work modulo alpha-conversion and implement the Barendregt variable convention. We derive them all from the simple structural induction principle on concrete terms and work out applications to some fundamental meta-theoretical results, such as the substitution lemma for alpha-conversion and the lemma on substitution composition. The whole work is implemented in Agda and the code is browsable here, the main result file is Substitution.html.
Authors:
- Ana Bove (Chalmers University of Technology)
- Ernesto Copello (Universidad ORT Uruguay)
- Maribel Fernandez (King's College London)
- Nora Szasz (Universidad ORT Uruguay)
- Álvaro Tasistro (Universidad ORT Uruguay)
Build Status
Agda compiler version 2.4.2.2 and standar library version 0.9