\begin{thebibliography}{10}
\bibitem{galton90}
Antony Galton.
\newblock {\em Logic for Information Technology}.
\newblock Wiley, 1990.
\bibitem{mgordon-hol}
M.~J.~C. Gordon and T.~F. Melham.
\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
Order Logic}.
\newblock Cambridge University Press, 1993.
\bibitem{mgordon79}
Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth.
\newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}.
\newblock LNCS 78. Springer, 1979.
\bibitem{haskell-tutorial}
Paul Hudak and Joseph~H. Fasel.
\newblock A gentle introduction to {Haskell}.
\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
\bibitem{haskell-report}
Paul Hudak, Simon~Peyton Jones, and Philip Wadler.
\newblock Report on the programming language {Haskell}: A non-strict, purely
functional language.
\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
\newblock Version 1.2.
\bibitem{huet75}
G.~P. Huet.
\newblock A unification algorithm for typed $\lambda$-calculus.
\newblock {\em Theoretical Computer Science}, 1:27--57, 1975.
\bibitem{miller-mixed}
Dale Miller.
\newblock Unification under a mixed prefix.
\newblock {\em Journal of Symbolic Computation}, 14(4):321--358, 1992.
\bibitem{nipkow-prehofer}
Tobias Nipkow and Christian Prehofer.
\newblock Type reconstruction for type classes.
\newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995.
\bibitem{nordstrom90}
Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
\newblock Oxford University Press, 1990.
\bibitem{paulson-natural}
Lawrence~C. Paulson.
\newblock Natural deduction as higher-order resolution.
\newblock {\em Journal of Logic Programming}, 3:237--258, 1986.
\bibitem{paulson87}
Lawrence~C. Paulson.
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
\newblock Cambridge University Press, 1987.
\bibitem{paulson-found}
Lawrence~C. Paulson.
\newblock The foundation of a generic theorem prover.
\newblock {\em Journal of Automated Reasoning}, 5(3):363--397, 1989.
\bibitem{paulson700}
Lawrence~C. Paulson.
\newblock {Isabelle}: The next 700 theorem provers.
\newblock In P.~Odifreddi, editor, {\em Logic and Computer Science}, pages
361--386. Academic Press, 1990.
\bibitem{paulson91}
Lawrence~C. Paulson.
\newblock {\em {ML} for the Working Programmer}.
\newblock Cambridge University Press, 1991.
\bibitem{paulson-handbook}
Lawrence~C. Paulson.
\newblock Designing a theorem prover.
\newblock In S.~Abramsky, D.~M. Gabbay, and T.~S.~E. Maibaum, editors, {\em
Handbook of Logic in Computer Science}, volume~2, pages 415--475. Oxford
University Press, 1992.
\bibitem{pelletier86}
F.~J. Pelletier.
\newblock Seventy-five problems for testing automatic theorem provers.
\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
\bibitem{reeves90}
Steve Reeves and Michael Clarke.
\newblock {\em Logic for Computer Science}.
\newblock Addison-Wesley, 1990.
\bibitem{suppes72}
Patrick Suppes.
\newblock {\em Axiomatic Set Theory}.
\newblock Dover, 1972.
\bibitem{wos-bledsoe}
Larry Wos.
\newblock Automated reasoning and {Bledsoe's} dream for the field.
\newblock In Robert~S. Boyer, editor, {\em Automated Reasoning: Essays in Honor
of {Woody Bledsoe}}, pages 297--342. Kluwer Academic Publishers, 1991.
\end{thebibliography}