Guo-Jun Qi, Charu Aggarwal, et al.
IEEE TPAMI
This paper recounts the origins of the a;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. © 2012 Springer Science+Business Media, LLC.
Guo-Jun Qi, Charu Aggarwal, et al.
IEEE TPAMI
Benjamin N. Grosof
AAAI-SS 1993
Bing Zhang, Mikio Takeuchi, et al.
NAACL 2025
Hagen Soltau, Lidia Mangu, et al.
ASRU 2011