\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{BoyerMoore79}
Robert~S. Boyer and J.~S. Moore.
\newblock {\em A Computational Logic}.
\newblock Academic Press, New York, 1979.

\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 {VLISP}: A Verified Implementation of Scheme.
\newblock {\em Lisp and Symbolic Computation}, 1993.
\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{OlivaRamsdellWand93}
Dino~P. Oliva, John~D. Ramsdell, and Mitchell Wand.
\newblock A Verified Compiler for VLISP PreScheme.
\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{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{WandOliva92}
Mitchell Wand and Dino~P. Oliva.
\newblock Proving the Correctness of Storage Representations.
\newblock In {\em {\lfp{1992}}}, pages 151--160, 1992.

\end{thebibliography}