1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\citeauthoryear{Abadi, Cardelli, Curien, and L{\'{e}}vy}{Abadi
4: et~al\mbox{.}}{1991}]{ACCL91}
5: {\sc Abadi, M.}, {\sc Cardelli, L.}, {\sc Curien, P.-L.}, {\sc and} {\sc
6: L{\'{e}}vy, J.-J.} 1991.
7: \newblock Explicit substitutions.
8: \newblock {\em Journal of Functional Programming\/}~{\em 1,\/}~4, 375--416.
9:
10: \bibitem[\protect\citeauthoryear{Baelde, Gacek, Miller, Nadathur, and
11: Tiu}{Baelde et~al\mbox{.}}{2007}]{BGMNT07}
12: {\sc Baelde, D.}, {\sc Gacek, A.}, {\sc Miller, D.}, {\sc Nadathur, G.}, {\sc
13: and} {\sc Tiu, A.} 2007.
14: \newblock The {B}edwyr system for model checking over syntactic expressions.
15: \newblock Available from the Computing Research Repository at
16: \url{http://arxiv.org/abs/cs.LO/0702116}.
17:
18: \bibitem[\protect\citeauthoryear{Benaissa, Briaud, Lescanne, and
19: Rouyer-Degli}{Benaissa et~al\mbox{.}}{1996}]{BBLR96}
20: {\sc Benaissa, Z.}, {\sc Briaud, D.}, {\sc Lescanne, P.}, {\sc and} {\sc
21: Rouyer-Degli, J.} 1996.
22: \newblock $\lambda\upsilon$, a calculus of explicit substitutions which
23: preserves strong normalization.
24: \newblock {\em Journal of Functional Programming\/}~{\em 6,\/}~5, 699--722.
25:
26: \bibitem[\protect\citeauthoryear{Bruijn}{Bruijn}{1972}]{debruijn72}
27: {\sc Bruijn, N.} 1972.
28: \newblock Lambda calculus notation with nameless dummies, a tool for automatic
29: formula manipulation, with application to the {Church-Rosser Theorem}.
30: \newblock {\em Indag. Math.\/}~{\em 34,\/}~5, 381--392.
31:
32: \bibitem[\protect\citeauthoryear{Cosmo, Kesner, and Polonovski}{Cosmo
33: et~al\mbox{.}}{2003}]{CKP03mscs}
34: {\sc Cosmo, R.~D.}, {\sc Kesner, D.}, {\sc and} {\sc Polonovski, E.} 2003.
35: \newblock Proof nets and explicit substitutions.
36: \newblock {\em Mathematical Structures in Computer Science\/}~{\em 13,\/}~3,
37: 409--450.
38:
39: \bibitem[\protect\citeauthoryear{Curien, Hardin, and L{\'e}vy}{Curien
40: et~al\mbox{.}}{1996}]{CHL96jacm}
41: {\sc Curien, P.-L.}, {\sc Hardin, T.}, {\sc and} {\sc L{\'e}vy, J.-J.} 1996.
42: \newblock Confluence properties of weak and strong calculi of explicit
43: substitutions.
44: \newblock {\em Journal of the ACM\/}~{\em 43,\/}~2, 362--397.
45:
46: \bibitem[\protect\citeauthoryear{David and Guillaume}{David and
47: Guillaume}{2001}]{DG01mscs}
48: {\sc David, R.} {\sc and} {\sc Guillaume, B.} 2001.
49: \newblock A $\lambda$-calculus with explicit weakening and explicit
50: substitution.
51: \newblock {\em Mathematical Structures for Computer Science\/}~{\em 11,\/}~1,
52: 169--206.
53:
54: \bibitem[\protect\citeauthoryear{Dershowitz}{Dershowitz}{1982}]{Dershowitz82}
55: {\sc Dershowitz, N.} 1982.
56: \newblock Orderings for term-rewriting systems.
57: \newblock {\em Theoretical Computer Science\/}~{\em 17,\/}~3, 279--301.
58:
59: \bibitem[\protect\citeauthoryear{Dowek, Hardin, and Kirchner}{Dowek
60: et~al\mbox{.}}{2000}]{DHK00}
61: {\sc Dowek, G.}, {\sc Hardin, T.}, {\sc and} {\sc Kirchner, C.} 2000.
62: \newblock Higher-order unification via explicit substitutions.
63: \newblock {\em Information and Computation\/}~{\em 157}, 183--235.
64:
65: \bibitem[\protect\citeauthoryear{Ferreira and Zantema}{Ferreira and
66: Zantema}{1995}]{ferreira94wellfoundedness}
67: {\sc Ferreira, M.} {\sc and} {\sc Zantema, H.} 1995.
68: \newblock Well-foundedness of term orderings.
69: \newblock In {\em Fourth International Workshop on Conditional Term Rewriting
70: Systems}, {N.~Dershowitz}, Ed. Lecture Notes in Computer Science, vol. 968.
71: Springer, 106--123.
72:
73: \bibitem[\protect\citeauthoryear{Field}{Field}{1990}]{Field90}
74: {\sc Field, J.} 1990.
75: \newblock On laziness and optimality in lambda interpreters: Tools for
76: specification and analysis.
77: \newblock In {\em Seventeenth Annual ACM Symposium on Principles of Programming
78: Languages}. ACM Press, 1--15.
79:
80: \bibitem[\protect\citeauthoryear{Gacek}{Gacek}{2006a}]{Gacek06coq}
81: {\sc Gacek, A.} 2006a.
82: \newblock A {{\it C}}{\it oq} proof of the termination of the reading and
83: merging rules in the suspension calculus.
84: \newblock
85: \url{http://www-users.cs.umn.edu/~agacek/pubs/gacek-masters/Termination/}.
86:
87: \bibitem[\protect\citeauthoryear{Gacek}{Gacek}{2006b}]{Gacek06msthesis}
88: {\sc Gacek, A.} 2006b.
89: \newblock The suspension calculus and its relationship to other explicit
90: treatments of subsubstitution in lambda calculi.
91: \newblock M.S.\ thesis, University of Minnesota.
92:
93: \bibitem[\protect\citeauthoryear{Guillaume}{Guillaume}{2000}]{Gui00jfp}
94: {\sc Guillaume, B.} 2000.
95: \newblock The $\lambda s_e$-calculus does not preserve strong normalisation.
96: \newblock {\em Journal of Functional Programming\/}~{\em 10,\/}~4, 321--325.
97:
98: \bibitem[\protect\citeauthoryear{Huet}{Huet}{1975}]{Huet75}
99: {\sc Huet, G.} 1975.
100: \newblock A unification algorithm for typed $\lambda$-calculus.
101: \newblock {\em Theoretical Computer Science\/}~{\em 1}, 27--57.
102:
103: \bibitem[\protect\citeauthoryear{Huet}{Huet}{1980}]{Huet80}
104: {\sc Huet, G.} 1980.
105: \newblock Confluent reductions: Abstract properties and applications to term
106: rewriting systems.
107: \newblock {\em Journal of the ACM\/}~{\em 27,\/}~4, 797--821.
108:
109: \bibitem[\protect\citeauthoryear{Kamareddine and Rios}{Kamareddine and
110: Rios}{1995}]{KR95}
111: {\sc Kamareddine, F.} {\sc and} {\sc Rios, A.} 1995.
112: \newblock A lambda-calculus `a la de bruijn with explicit substitutions.
113: \newblock In {\em Seventh International Conference on Programming Languages:
114: Implementations, Logics and Programs (PLILP)}. Lecture Notes in Computer
115: Science, vol. 982. Springer, 45--62.
116:
117: \bibitem[\protect\citeauthoryear{Kamareddine and R\'{i}os}{Kamareddine and
118: R\'{i}os}{1997}]{KR97}
119: {\sc Kamareddine, F.} {\sc and} {\sc R\'{i}os, A.} 1997.
120: \newblock Extending the $\lambda$-calculus with explicit substitution which
121: preserves strong normalization into a confluent calculus on open terms.
122: \newblock {\em Journal of Functional Programming\/}~{\em 7,\/}~4, 395--420.
123:
124: \bibitem[\protect\citeauthoryear{Liang, Nadathur, and Qi}{Liang
125: et~al\mbox{.}}{2004}]{liang-04-choices}
126: {\sc Liang, C.}, {\sc Nadathur, G.}, {\sc and} {\sc Qi, X.} 2004.
127: \newblock Choices in representation and reduction strategies for lambda terms
128: in intensional contexts.
129: \newblock {\em J. Autom. Reasoning\/}~{\em 33,\/}~2, 89--132.
130:
131: \bibitem[\protect\citeauthoryear{Mellies}{Mellies}{1995}]{Mellies95}
132: {\sc Mellies, P.-A.} 1995.
133: \newblock Typed $\lambda$-calculi with explicit substitutions may not
134: terminate.
135: \newblock In {\em Second International Conference on Typed Lambda Calculi and
136: Applications}, {M.~Dezani-Ciancaglini} {and} {G.~Plotkin}, Eds. Lecture Notes
137: in Computer Science, vol. 902. Springer, 328--334.
138:
139: \bibitem[\protect\citeauthoryear{Miller}{Miller}{2000}]{Mil00cl}
140: {\sc Miller, D.} 2000.
141: \newblock Abstract syntax for variable binders: An overview.
142: \newblock In {\em Proceedings of the First International Conference on
143: Computational Logic}, {J.~Lloyd}, Ed. Lecture Notes in Artificial
144: Intelligence, vol. 1861. Springer, 239--253.
145:
146: \bibitem[\protect\citeauthoryear{Mu{\~{n}}oz}{Mu{\~{n}}oz}{1996}]{Munoz96}
147: {\sc Mu{\~{n}}oz, C.} 1996.
148: \newblock Confluence and preservation of strong normalization in an explicit
149: substitution calculus.
150: \newblock In {\em Eleventh Annual IEEE Symposium on Logic in Computer Science}.
151: IEEE Computer Society Press, 440--447.
152:
153: \bibitem[\protect\citeauthoryear{Nadathur}{Nadathur}{1999}]{Nad99jflp}
154: {\sc Nadathur, G.} 1999.
155: \newblock A fine-grained notation for lambda terms and its use in intensional
156: operations.
157: \newblock {\em Journal of Functional and Logic Programming\/}~{\em 1999,\/}~2
158: (March).
159:
160: \bibitem[\protect\citeauthoryear{Nadathur and Mitchell}{Nadathur and
161: Mitchell}{1999}]{NM99cade}
162: {\sc Nadathur, G.} {\sc and} {\sc Mitchell, D.~J.} 1999.
163: \newblock System description: {T}eyjus---a compiler and abstract machine based
164: implementation of $\lambda${P}rolog.
165: \newblock In {\em Automated Deduction--{CADE}-16}, {H.~Ganzinger}, Ed. Lecture
166: Notes in Artificial Intelligence, vol. 1632. Springer, 287--291.
167:
168: \bibitem[\protect\citeauthoryear{Nadathur and Wilson}{Nadathur and
169: Wilson}{1998}]{NW98tcs}
170: {\sc Nadathur, G.} {\sc and} {\sc Wilson, D.} 1998.
171: \newblock A notation for lambda terms: A generalization of environments.
172: \newblock {\em Theoretical Computer Science\/}~{\em 198,\/}~1-2, 49--98.
173:
174: \bibitem[\protect\citeauthoryear{Pfenning and Elliott}{Pfenning and
175: Elliott}{1988}]{PE88pldi}
176: {\sc Pfenning, F.} {\sc and} {\sc Elliott, C.} 1988.
177: \newblock Higher-order abstract syntax.
178: \newblock In {\em Proceedings of the {ACM}-{SIGPLAN} Conference on Programming
179: Language Design and Implementation}. {ACM} Press, 199--208.
180:
181: \bibitem[\protect\citeauthoryear{Shao, League, and Monnier}{Shao
182: et~al\mbox{.}}{1998}]{shao98:imp}
183: {\sc Shao, Z.}, {\sc League, C.}, {\sc and} {\sc Monnier, S.} 1998.
184: \newblock Implementing typed intermediate languages.
185: \newblock In {\em Proc. 1998 {ACM} {SIGPLAN} International Conference on
186: Functional Programming ({ICFP}'98)}. ACM Press, 313--323.
187:
188: \end{thebibliography}
189: