\begin{thebibliography}{BTCGS91}

\bibitem[AC94]{Abadi94}
Mart{\'{\i}}n Abadi and Luca Cardelli.
\newblock A theory of primitive objects.
\newblock Draft paper available from gatekeeper.pa.dec.com, February 1994.

\bibitem[ACCL91]{Abadi91}
Mart\'{\i}n Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques
  L\'{e}vy.
\newblock Explicit substitutions.
\newblock {\em Journal of Functional Programming}, 1(4):375--416, October 1991.

\bibitem[Bac91]{Bachmair91}
Leo Bachmair.
\newblock {\em Canonical Equational Proofs}.
\newblock Birk{\"a}user, Boston, 1991.

\bibitem[BTCGS91]{Breazutannen91}
Val Breazu-Tannen, Thierry Coquand, Carl Gunter, and Andre Scedrov.
\newblock Inheritance as implicit coercion.
\newblock {\em Information and Computation}, 93:172--221, 1991.

\bibitem[CC77]{Cousot77}
Patrick Cousot and Radhia Cousot.
\newblock Abstract interpretation: A unified lattice model for static analysis
  of programs by construction or approximation of fixpoints.
\newblock In {\em Proceedings of the Fourth Annual {ACM} Symposium on
  Principles of Programming Languages}, pages 238--252. ACM, 1977.

\bibitem[CCM87]{Cousineau87}
Guy Cousineau, Pierre-Louis Curien, and Michel Mauny.
\newblock The categorical abstract machine.
\newblock {\em Science of Computer Programming}, 8, May 1987.

\bibitem[CDCV81]{Coppo81}
Mario Coppo, Maria Dezani-Ciancaglini, and B.~Venneri.
\newblock Functional character of solvable terms.
\newblock {\em Zeitschrift f{\"u}r mathematische Logic und Grundlagen der
  Mathematik}, 27:45--58, 1981.

\bibitem[Fil94]{Filinski94}
Andrzej Filinski.
\newblock Representing monads.
\newblock In H.-J. Boehm, editor, {\em Conference Record of the 21st Symposium
  on Principles of Programming Languages}, pages 446--457, Portland, Oregon,
  January 1994. ACM Press.

\bibitem[Hen93]{Henglein93}
Fritz Henglein.
\newblock Type inference with polymorphic recursion.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  15(2):253--289, April 1993.

\bibitem[HM94]{Hankin94}
Chris Hankin and Daniel~Le M\'etayer.
\newblock Deriving algorithms from type inference systems: Application to
  strictness analysis.
\newblock In {\em Proceedings of the Twenty-First Annual ACM Symposium on
  Principles of Programming Languages, Portland}, pages 202--212. ACM, January
  1994.

\bibitem[Lau93]{Launchbury93}
John Launchbury.
\newblock A natural semantics for lazy evaluation.
\newblock In S.~Graham, editor, {\em Conference Record of the {20th} Annual
  Symposium on Principles of Programming Languages}, pages 144--154,
  Charleston, South Carolina, January 1993. ACM Press.

\bibitem[MNPS91]{Miller91b}
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov.
\newblock Uniform proofs as a foundation for logic programming.
\newblock {\em Annals of Pure and Applied Logic}, 51:125--157, 1991.

\bibitem[MTH90]{Milner90}
Robin Milner, Mads Tofte, and Robert Harper.
\newblock {\em The Definition of Standard {ML}}.
\newblock MIT Press, Cambridge, Massachusetts, 1990.

\bibitem[NN92]{Nielson92}
Flemming Nielson and Hanne~Riis Nielson.
\newblock {\em Two-Level Functional Languages}.
\newblock Cambridge University Press, 1992.

\bibitem[Ode94]{Odersky94}
Martin Odersky.
\newblock A functional theory of local names.
\newblock In H.-J. Boehm, editor, {\em Conference Record of the 21st Symposium
  on Principles of Programming Languages}, pages 48--59, Portland, Oregon,
  January 1994. ACM Press.

\bibitem[PA93]{Plotkin93}
Gordon Plotkin and Mart{\'{\i}}n Abadi.
\newblock A logic for parametric polymorphism.
\newblock In M.~Bezem and J.F. Groote, editors, {\em Proceedings of the
  International Conference on Typed Lambda Calculi and Applications,
  {TLCA'93}}, pages 361--375, Utrecht, The Netherlands, March 1993.
  Springer-Verlag LNCS 664.

\bibitem[Rey72]{Reynolds72}
John~C. Reynolds.
\newblock Definitional interpreters for higher-order programming languages.
\newblock In {\em Proceedings of the 25th ACM National Conference}, pages
  717--740, New York, 1972. ACM.

\bibitem[Rey88]{Reynolds88b}
John~C. Reynolds.
\newblock Preliminary design of the programming language {Forsythe}.
\newblock Technical Report CMU-CS-88-159, Carnegie Mellon University,
  Pittsburgh, Pennsylvania, June 1988.

\bibitem[Rey91]{Reynolds91}
John~C. Reynolds.
\newblock The coherence of languages with intersection types.
\newblock In T.~Ito and A.~R. Meyer, editors, {\em International Conference on
  Theoretical Aspects of Computer Software}, pages 675--700, Sendai, Japan,
  September 1991. Springer-Verlag LNCS 526.

\bibitem[Sny91]{Snyder91}
Wayne Snyder.
\newblock {\em A Proof Theory for General Unification}.
\newblock Birkh{\"a}user, 1991.

\end{thebibliography}