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

Alpha-Structural 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
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE (1571-0661). Vol. 323 (2016), p. 109-124.
[Artikel, refereegranskad vetenskaplig]

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.

Nyckelord: substitution



Denna post skapades 2017-01-27. Senast ändrad 2017-07-07.
CPL Pubid: 247760

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)