Abstract : 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.
https://hal.inria.fr/hal-00763399
Contributeur : Frederic Lang
<>
Soumis le : lundi 10 décembre 2012 - 16:49:10
Dernière modification le : mercredi 11 avril 2018 - 01:54:03
