CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Principles of Alpha-Induction and Recursion for the Lambda Calculus in Constructive Type Theory

Ernesto Copello ; Alvaro Tasistro ; Nora Szasz ; Ana Bove (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Maribel Fernandez
LSFA p. 16. (2015)
[Konferensbidrag, refereegranskat]

We formulate principles of induction and recursion for a variant of lambda calculus in its original syntax (i.e., with only one sort of 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.



Denna post skapades 2015-12-08.
CPL Pubid: 227632