\def\popl#1{{\it {Conf. Rec. #1 ACM Symposium on Principles of Programming
  Languages}\/}} \def\lics#1{{\it Proc. #1 IEEE Symposium on Logic in Computer
  Science\/}} \def\lfp#1{{\it Proc. #1 ACM Symposium on Lisp and Functional
  Programming}} \def\tr{Northeastern University College of Computer Science
  Technical Report NU-CCS-} \def\mfcs#1{{\it Mathematical Foundations of
  Computer Science #1}}
\begin{thebibliography}{10}

\bibitem{Barendregt81}
Henk~P. Barendregt.
\newblock {\em The Lambda Calculus: Its Syntax and Semantics}.
\newblock North-Holland, Am\-ster\-dam, 1981.

\bibitem{BoyerMoore79}
Robert~S. Boyer and J.~S. Moore.
\newblock {\em A Computational Logic}.
\newblock Academic Press, New York, 1979.

\bibitem{Burstall69}
Rod~M. Burstall.
\newblock Proving Properties of Programs by Structural Induction.
\newblock {\em Computer Journal}, 12(1):41--48, February 1969.

\bibitem{Bolek91}
Boleslaw Ciesielski and Mitchell Wand.
\newblock Using the Theorem Prover Isabelle-91 to Verify a Simple Proof of
  Compiler Correctness.
\newblock Technical Report NU-CCS-91-20, Northeastern University College of
  Computer Science, December 1991.

\bibitem{Clinger84}
William Clinger.
\newblock The Scheme 311 Compiler: An Exercise in Denotational Semantics.
\newblock In {\em {\lfp{1984}}}, pages 356--364, August 1984.

\bibitem{FriedmanEtAl92}
Daniel~P. Friedman, Mitchell Wand, and Christopher~T. Haynes.
\newblock {\em Essentials of Programming Languages}.
\newblock MIT Press, Cambridge, MA, 1992.
\newblock Also McGraw-Hill, Chicago, 1992.

\bibitem{GuttmanSwarupRamsdell93}
J.~D. Guttman, V.~Swarup, and J.~Ramsdell.
\newblock The {VLISP} Verified Scheme System.
\newblock {\em Lisp and Symbolic Computation}, 1994.
\newblock Submitted for publication.

\bibitem{Hannan92}
John Hannan and Frank Pfenning.
\newblock Compiler Verification in {LF}.
\newblock In Andre Scedrov, editor, {\em Proceedings of the Seventh Annual IEEE
  Symposium on Logic in Computer Science}, pages 407--418. {IEEE} Computer
  Society Press, 1992.

\bibitem{HarperHonsellPlotkin93}
Robert Harper, Furio Honsell, and Gordon Plotkin.
\newblock A Framework for Defining Logics.
\newblock {\em Journal of the ACM}, 40(1):143--184, 1993.
\newblock preliminary version appeared in {\lics{2nd}}, 1987, 194--204.

\bibitem{Hughes82}
R.~J.~M. Hughes.
\newblock Super Combinators: A New Implementation Method for Applicative
  Languages.
\newblock In {\em {\lfp{1982}}}, pages 1--10, 1982.

\bibitem{Meyer82}
Albert~R. Meyer.
\newblock What Is a Model of the Lambda Calculus?
\newblock {\em Information and Control}, 52:87--122, 1982.

\bibitem{NadathurMiller88}
G.~Nadathur and D.~Miller.
\newblock An Overview of {$\lambda$-Prolog}.
\newblock In Kowalski and Bowen, editors, {\em Logic Programming: Proceedings
  of the 5th International Conference and Symposium}, pages 810--827,
  Cambridge, MA, 1988. MIT Press.

\bibitem{Nipkow91}
Tobias Nipkow.
\newblock Nigher-Order Critical Pairs.
\newblock In {\em {\lics{6th}}}, pages 342--349, 1991.

\bibitem{OlivaRamsdellWand94}
Dino~P. Oliva, John~D. Ramsdell, and Mitchell Wand.
\newblock The VLISP Verified PreScheme Compiler.
\newblock {\em Lisp and Symbolic Computation}, 1994.
\newblock submitted for publication.

\bibitem{Paulson89}
Lawrence~C. Paulson.
\newblock The Foundation of a Generic Theorem Prover.
\newblock {\em Journal of Automated Reasoning}, 5:363--397, 1989.

\bibitem{Pfenning91}
Frank Pfenning.
\newblock Logic Programming in the {LF} Logical Framework.
\newblock In G.~Huet and G.~Plotkin, editors, {\em Logical Frameworks}, pages
  149--181. Cambridge University Press, 1991.

\bibitem{Talcott93}
Carolyn Talcott.
\newblock A Theory of Binding Structures and Applications to Rewriting.
\newblock {\em Theoretical Computer Science}, 112:99--143, 1993.

\bibitem{Wand82c}
Mitchell Wand.
\newblock Deriving Target Code as a Representation of Continuation Semantics.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  4(3):496--517, July 1982.

\bibitem{Wand82b}
Mitchell Wand.
\newblock Semantics-Directed Machine Architecture.
\newblock In {\em {\popl{9th}}}, pages 234--241, 1982.

\bibitem{Wand83b}
Mitchell Wand.
\newblock Loops in Combinator-Based Compilers.
\newblock {\em Information ~and Control}, 57(2--3):148--164, May/June 1983.

\bibitem{WandConcur94}
Mitchell Wand.
\newblock Compiler Correctness for Parallel Languages.
\newblock in preparation, August 1994.

\bibitem{WandOliva92}
Mitchell Wand and Dino~P. Oliva.
\newblock Proving the Correctness of Storage Representations.
\newblock In {\em {\lfp{1992}}}, pages 151--160, 1992.

\bibitem{WandWang90}
Mitchell Wand and Zheng-Yu Wang.
\newblock Conditional Lambda-Theories and the Verification of Static Properties
  of Programs.
\newblock In {\em {\lics{5th}}}, pages 321--332, 1990.

\end{thebibliography}