References

[ACCL90]

Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. In Proceedings of the 17th Annual ACM Symposium on Principles of Programming Languages, pages 31–46, San Francisco, California, January 1990.

[BBC⁺99]

Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, Henri Laulhère, Cesar Muñoz, Chetan Murthy, Catherine Parent-Vigouroux, Patrick Loiseleur, Christine Paulin-Mohring, Amokrane Saïbi, and Benjamin Werner. The Coq proof assistant — reference manual. Disponible en http://coq.inria.fr/doc/main.html., décembre 1999. Version 6.3.1.

[CHL91]

Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Rapport de recherche, INRIA, 1991.

[Dil88]

Antoni Diller. Compiling Functional Languages. John Wiley and Sons, 1988.

[DJ90]

Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 243–320. Elsevier Science Publishers b.v., 1990.

[LRD94]

Pierre Lescanne and Jocelyne Rouyer-Degli. From λσ to λυ: a journey through calculi of explicit substitutions. In Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages, 1994.

[Mel95]

Paul-André Melliès. Typed lambda-calculi with explicit substitutions may not terminate. In M. Dezani-Ciancaglini and G. Plotkin, editors, 2nd International Conference on Typed Lambda-Calculi and Applications (TLCA'95), pages 328–334, Edinburgh, UK, April 1995. Springer Verlag LNCS 902.

[Río93]

Alejandro Ríos. Contributions à l'étude des lambda-calculs avec substitutions explicites. PhD thesis, École Normale Supérieure, December 1993.