On explicit substitution with names

K.H. Rose, R. Bloo, F. Lang

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

1 Citaat (Scopus)


This paper recounts the origins of the ¿x family of calculi of explicit substitution with proper variable names, including the original result of preservation of strong ß-normalization based on the use of synthetic reductions for garbage collection. We then discuss the properties of a variant of the calculus which is also confluent for "open" terms (with meta-variables), and verify that a version with garbage collection preserves strong ß-normalization (as is the state of the art), and we summarize the relationship with other efforts on using names and garbage collection rules in explicit substitution.
Originele taal-2Engels
Pagina's (van-tot)275-300
TijdschriftJournal of Automated Reasoning
Nummer van het tijdschrift2
StatusGepubliceerd - 2012

Vingerafdruk Duik in de onderzoeksthema's van 'On explicit substitution with names'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit