1: \begin{thebibliography}{BBLRD96}
2:
3: \bibitem[ACCL91]{abadi-91-explicit}
4: Mart{\'{\i}}n Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques
5: L{\'{e}}vy.
6: \newblock Explicit substitutions.
7: \newblock {\em Journal of Functional Programming}, 1(4):375--416, 1991.
8:
9: \bibitem[ARK03]{rincon-03-applying}
10: Mauricio Ayala-Rinc\'on and Fairouz Kamareddine.
11: \newblock On applying the $\lambda s_e$-style of unification for simply-typed
12: higher order unification in the pure $\lambda$-calculus.
13: \newblock {\em Sociedade Brasileira de Matem\'atica}, 24:1--22, July 2003.
14:
15: \bibitem[Bar81]{barendregt-81-lambda}
16: H.~P. Barendregt.
17: \newblock {\em The Lambda Calculus: Its Syntax and Semantics}.
18: \newblock North Holland Publishing Co., 1981.
19:
20: \bibitem[BBLRD96]{benaissa-96-upsilon}
21: Z.~Benaissa, D.~Briaud, P.~Lescanne, and J.~Rouyer-Degli.
22: \newblock $\lambda\upsilon$, a calculus of explicit substitutions which
23: preserves strong normalization.
24: \newblock {\em Journal of Functional Programming}, 6(5):699--722, 1996.
25:
26: \bibitem[CCM87]{cousineau-87-cam}
27: G.~Cousineau, P-L. Curien, and M.~Mauny.
28: \newblock The categorical abstract machine.
29: \newblock {\em The Science of Programming}, 8(2):173--202, 1987.
30:
31: \bibitem[CHL96]{curien-96-confluence}
32: Pierre-Louis Curien, Th{\'e}r{\`e}se Hardin, and Jean-Jacques L{\'e}vy.
33: \newblock Confluence properties of weak and strong calculi of explicit
34: substitutions.
35: \newblock {\em Journal of the ACM}, 43(2):362--397, 1996.
36:
37: \bibitem[Chu40]{church-40-types}
38: Alonzo Church.
39: \newblock A formulation of the simple theory of types.
40: \newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.
41:
42: \bibitem[dB72]{debruijn-72-nameless}
43: N.G. de~Bruijn.
44: \newblock Lambda-calculus notation with nameless dummies: a tool for automatic
45: formula manipulation with application to the {Church-Rosser} theorem.
46: \newblock {\em Indag. Math.}, 34(5):381--392, 1972.
47:
48: \bibitem[Der82]{dershowitz-82-orderings}
49: Nachum Dershowitz.
50: \newblock Orderings for term-rewriting systems.
51: \newblock {\em Theoretical Computer Science}, 17(3):279--301, 1982.
52:
53: \bibitem[DG01a]{guillaume-01-weakening}
54: R.~David and B.~Guillaume.
55: \newblock A $\lambda$-calculus with explicit weakening and explicit
56: substitution.
57: \newblock {\em Mathematical Structures in Computer Science}, 11(1), 2001.
58:
59: \bibitem[DG01b]{david-01-calculus}
60: Ren{\'e} David and Bruno Guillaume.
61: \newblock A lambda-calculus with explicit weakening and explicit substitution.
62: \newblock {\em Mathematical Structures in Computer Science}, 11(1):169--206,
63: 2001.
64:
65: \bibitem[DHK95]{dowek-95-higherorder}
66: Gilles Dowek, Th{\'e}r{\`e}se Hardin, and Claude Kirchner.
67: \newblock Higher-order unification via explicit substitutions.
68: \newblock In D.~Kozen, editor, {\em Proceedings of the Tenth Annual Symposium
69: on Logic in Computer Science}, pages 366--374, San Diego, California, June
70: 1995. IEEE Computer Society Press.
71:
72: \bibitem[Fie90]{field-90-laziness}
73: John Field.
74: \newblock On laziness and optimality in lambda interpreters: Tools for
75: specification and analysis.
76: \newblock In {\em Seventeenth Annual ACM Symposium on Principles of Programming
77: Languages}, pages 1--15. ACM Press, January 1990.
78:
79: \bibitem[FZ95]{ferreira-94-wellfoundedness}
80: M.C.F. Ferreira and H.~Zantema.
81: \newblock Well-foundedness of term orderings.
82: \newblock In N.~Dershowitz, editor, {\em Fourth International Workshop on
83: Conditional Term Rewriting Systems}, volume 968 of {\em Lecture Notes in
84: Computer Science}, pages 106--123. Springer, 1995.
85:
86: \bibitem[GL02]{gregoire-02-compiled}
87: B.~Gr\'{e}goire and X.~Leroy.
88: \newblock A compiled implementation of strong reduction.
89: \newblock In {\em Proceedings of the Seventh ACM SIGPLAN International
90: Conference on Functional Programming}, pages 235--246, Pittsburgh, October
91: 2002.
92:
93: \bibitem[Gui00]{guillaume-00-preserve}
94: B.~Guillaume.
95: \newblock The $\lambda s_e$-calculus does not preserve strong normalisation.
96: \newblock {\em Journal of Functional Programming}, 10(4):321--325, July 2000.
97:
98: \bibitem[Har89]{hardin-89-confluence}
99: Th{\'e}r{\`e}se Hardin.
100: \newblock Confluence results for the pure strong categorical logic ccl:
101: lambda-calculi as subsystems of ccl.
102: \newblock {\em Theor. Comput. Sci.}, 65(3):291--342, 1989.
103:
104: \bibitem[HHP93]{harper-93-LF}
105: Robert Harper, Furio Honsell, and Gordon Plotkin.
106: \newblock A framework for defining logics.
107: \newblock {\em J. ACM}, 40(1):143--184, 1993.
108:
109: \bibitem[Hue75]{huet-75-unification}
110: G\'erard Huet.
111: \newblock A unification algorithm for typed $\lambda$-calculus.
112: \newblock {\em Theoretical Computer Science}, 1:27--57, 1975.
113:
114: \bibitem[Hue80]{huet-80-confluent}
115: G\'erard Huet.
116: \newblock Confluent reductions: Abstract properties and applications to term
117: rewriting systems.
118: \newblock {\em Journal of the ACM}, 27(4):797--821, October 1980.
119:
120: \bibitem[KR95]{kamareddine-95-calculus}
121: Fairouz Kamareddine and Alejandro Rios.
122: \newblock A lambda-calculus `a la de bruijn with explicit substitutions.
123: \newblock In {\em {PLILP}}, pages 45--62, 1995.
124:
125: \bibitem[KR97]{kamareddine-97-extending}
126: Fairouz Kamareddine and Alejandro Rios.
127: \newblock Extending a lambda-calculus with explicit substitution which
128: preserves strong normalisation into a confluent calculus on open terms.
129: \newblock {\em Journal of Functional Programming}, 7(4):395--420, 1997.
130:
131: \bibitem[Lan66]{landin-66-next700}
132: P.~J. Landin.
133: \newblock The next 700 programming languages.
134: \newblock {\em Commun. ACM}, 9(3):157--166, 1966.
135:
136: \bibitem[LNQ04]{liang-04-choices}
137: Chuck Liang, Gopalan Nadathur, and Xiaochu Qi.
138: \newblock Choices in representation and reduction strategies for lambda terms
139: in intensional contexts.
140: \newblock {\em J. Autom. Reasoning}, 33(2):89--132, 2004.
141:
142: \bibitem[Mel95]{mellies-95-terminate}
143: Paul-Andr{\'e} Mellies.
144: \newblock Typed $\lambda$-calculi with explicit substitutions may not
145: terminate.
146: \newblock In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, {\em
147: Typed Lambda Calculi and Applications: Second International Conference on
148: Typed Lambda Calculi and Applications}, pages 328--334. Springer, 1995.
149: \newblock Lecture Notes in Computer Science 902.
150:
151: \bibitem[Nad99]{nadathur-99-finegrained}
152: Gopalan Nadathur.
153: \newblock A fine-grained notation for lambda terms and its use in intensional
154: operations.
155: \newblock {\em Journal of Functional and Logic Programming}, 1999(2), March
156: 1999.
157:
158: \bibitem[NM91]{nadathur-91-overview}
159: Gopalan Nadathur and Dale Miller.
160: \newblock An overview of $\lambda$prolog.
161: \newblock In R.~A. Kowalski and K.~A. Bowen, editors, {\em Logic Programming:
162: Proceedings of the 5th International Conference and Symposium}, pages
163: 810--827, Cambridge, MA, 1991. MIT Press.
164:
165: \bibitem[NP92]{nadathur-92-type}
166: Gopalan Nadathur and Frank Pfenning.
167: \newblock The type system of a higher-order logic programming language.
168: \newblock In {\em Types in Logic Programming}, pages 245--283. MIT Press, 1992.
169:
170: \bibitem[NW90]{nadathur-90-representation}
171: Gopalan Nadathur and Debra~Sue Wilson.
172: \newblock A representation of lambda terms suitable for operations on their
173: intensions.
174: \newblock In {\em Proceedings of the 1990 ACM Conference on Lisp and Functional
175: Programming}, pages 341--348. ACM Press, 1990.
176:
177: \bibitem[NW98]{nadathur-98-suspension}
178: Gopalan Nadathur and Debra~Sue Wilson.
179: \newblock A notation for lambda terms: A generalization of environments.
180: \newblock {\em Theoretical Computer Science}, 198(1-2):49--98, 1998.
181:
182: \bibitem[PS99]{pfenning-99-twelf}
183: Frank Pfenning and Carsten Sch{\"u}rmann.
184: \newblock System description: Twelf --- {A} meta-logical framework for
185: deductive systems.
186: \newblock In H.~Ganzinger, editor, {\em Proceedings of the 16th International
187: Conference on Automated Deduction ({CADE}-16)}, pages 202--206, Trento,
188: Italy, 1999. Springer-Verlag LNAI 1632.
189:
190: \bibitem[Sto81]{stoy-81-denotational}
191: Joseph~E. Stoy.
192: \newblock {\em Denotational Semantics: The Scott-Strachey Approach to
193: Programming Language Theory}.
194: \newblock MIT Press, Cambridge, MA, USA, 1981.
195:
196: \end{thebibliography}
197: