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 apply the Barendregt variable convention. We derive them all from the simple structural induction principle and apply them to get some fundamental meta-theoretical results, such as the substitution lemma for alpha-conversion and the result of substitution composition. The whole work is implemented in Agda, and is browsable here.

Documentation

• Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory. Electr. Notes Theor. Comput. Sci. 323: 109-124 (2016)

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 in Travis CI :

Agda compiler version 2.5.1 and standard library version 0.12

Updated version of this work:

Machine-checked proof of the Church-Rosser theorem for Lambda-Calculus using the Barendregt Variable Convention in Constructive Type Theory, Electronic Notes in Theoretical Computer Science,2018 in press.

Project