On Explicit Substitution with Names

Kristoffer H. Rose 1 Roel Bloo 2 Frederic Lang 3, *
* Corresponding author
3 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Document type :
Journal articles
Journal of Automated Reasoning, Springer Verlag, 2012, Special Issue: Theory and Applications of Abstraction, Substitution and Naming, 49 (2), pp.275-300. <http://www.springerlink.com/content/l6g664q3pr3863xk/>. <10.1007/s10817-011-9222-5>
Liste complète des métadonnées

https://hal.inria.fr/hal-00763399
Contributor : Frederic Lang <>
Submitted on : Monday, December 10, 2012 - 4:49:10 PM
Last modification on : Wednesday, October 7, 2015 - 1:16:29 AM

Identifiers

Collections

Citation

Kristoffer H. Rose, Roel Bloo, Frederic Lang. On Explicit Substitution with Names. Journal of Automated Reasoning, Springer Verlag, 2012, Special Issue: Theory and Applications of Abstraction, Substitution and Naming, 49 (2), pp.275-300. <http://www.springerlink.com/content/l6g664q3pr3863xk/>. <10.1007/s10817-011-9222-5>. <hal-00763399>

Share

Metrics

Consultations de la notice

193