M. Abadi, L. Cardelli, P.-L. Curien & J.-J. Lévy (1991):
Explicit Substitutions.
J. Funct. Prog. 1,
pp. 31–46.
Z. Benaissa, D. Briaud, P. Lescanne & J. Rouyer-Degli (1996):
λυ, a Calculus of Explicit Substitutions which Preserves Strong Normalisation.
J. Funct. Prog. 6(5),
pp. 699–722.
R. Bloo & H. Geuvers (1999):
Explicit substitution on the edge of strong normalization.
Theor. Comput. Sci. 211(1-2),
pp. 375–395.
R. Bloo & K. H. Rose (1995):
Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection.
In: CSN-95: Computing Science in the Netherlands,
pp. 62–72.
N. G. de Bruijn (1972):
Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem.
Indagationes Mathematicae 34,
pp. 381–392.
N. G. de Bruijn (1978):
A namefree λ calculus with facilities for internal definition of expressions and segments.
Tech. Rep. TH-Report 78-WSK-03, Dept. of Mathematics, Technical University of Eindhoven.
P.-L. Curien, Th. Hardin & J.-J. Lévy (1996):
Confluence properties of weak and strong calculi of explicit substitutions.
Journal of the ACM 43(2),
pp. 362–397.
G. Dowek, Th. Hardin & C. Kirchner (2000):
Higher order unification via explicit substitutions.
Inf. Comput. 157(1-2),
pp. 183–235.
M. Fernández & M. J. Gabbay (2007):
Nominal rewriting.
Inf. Comput. 205(6),
pp. 917–965.
M. J. Gabbay & A. M. Pitts (2002):
A new approach to abstract syntax with variable binding.
Formal Aspects of Computing 13,
pp. 341–363.
F. Kamareddine & A. Ríos (1995):
A Lambda-Calculus à la de Bruijn with Explicit Substitutions.
In: PLILP '95: Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs, Lecture Notes in Computer Science 982,
pp. 45–62.
F. Kamareddine & A. Ríos (1997):
Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms.
J. Funct. Prog. 7(4),
pp. 395–420.
F. Kamareddine & A. Ríos (1998):
Bridging de Bruijn Indices and Variable Names in Explicit Substitutions Calculi.
Logic Journal of the IGPL 6(6),
pp. 843–874.
D. Kesner (2008):
Perpetuality for Full and Safe Composition (in a Constructive Setting).
In: ICALP '08: Proceedings of the 35th international colloquium on Automata, Languages and Programming, Part II.
Springer-Verlag,
Berlin, Heidelberg,
pp. 311–322.
D. Kesner (2009):
A Theory of Explicit Substitutions with Safe and Full Composition.
Logical Methods in Computer Science 5(3:1),
pp. 1–29.
P. Lescanne (1994):
From λσ to λυ: a journey through calculi of explicit substitutions.
In: POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on principles of programming languages.
ACM,
New York, NY, USA,
pp. 60–69.
P.-A. Melliès (1995):
Typed lambda-calculi with explicit substitutions may not terminate.
In: TLCA '95: Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 902,
pp. 328–334.
A. Mendelzon (2010):
Una curiosa versión de λ_dB basada en ``swappings'': aplicación a traducciones entre cálculos de sustituciones explícitas con nombres e índices.
Master's thesis, FCEyN, Univ. de Buenos Aires.
Available at http://publi.dc.uba.ar/publication/pdffile/128/tesis_amendelzon.pdf.
A. Ríos (1993):
Contributions à l'étude des Lambda-calculus avec Substitutions Explicites.
Ph.D. thesis.
Université Paris 7.
eptcs@eptcs.org