105

1 
\begin{thebibliography}{10}


2 


3 
\bibitem{galton90}


4 
Antony Galton.


5 
\newblock {\em Logic for Information Technology}.


6 
\newblock Wiley, 1990.


7 

359

8 
\bibitem{mgordonhol}


9 
M.~J.~C. Gordon and T.~F. Melham.


10 
\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher


11 
Order Logic}.


12 
\newblock Cambridge University Press, 1993.

105

13 

359

14 
\bibitem{mgordon79}

105

15 
Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth.


16 
\newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}.

1878

17 
\newblock LNCS 78. Springer, 1979.

105

18 


19 
\bibitem{haskelltutorial}


20 
Paul Hudak and Joseph~H. Fasel.


21 
\newblock A gentle introduction to {Haskell}.

359

22 
\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.

105

23 


24 
\bibitem{haskellreport}


25 
Paul Hudak, Simon~Peyton Jones, and Philip Wadler.


26 
\newblock Report on the programming language {Haskell}: A nonstrict, purely


27 
functional language.

359

28 
\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.

105

29 
\newblock Version 1.2.


30 


31 
\bibitem{huet75}


32 
G.~P. Huet.


33 
\newblock A unification algorithm for typed $\lambda$calculus.


34 
\newblock {\em Theoretical Computer Science}, 1:2757, 1975.


35 

359

36 
\bibitem{millermixed}

105

37 
Dale Miller.


38 
\newblock Unification under a mixed prefix.


39 
\newblock {\em Journal of Symbolic Computation}, 14(4):321358, 1992.


40 


41 
\bibitem{nipkowprehofer}


42 
Tobias Nipkow and Christian Prehofer.

1182

43 
\newblock Type reconstruction for type classes.

1224

44 
\newblock {\em Journal of Functional Programming}, 5(2):201224, 1995.

105

45 


46 
\bibitem{nordstrom90}


47 
Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.


48 
\newblock {\em Programming in {MartinL\"of}'s Type Theory. An Introduction}.

359

49 
\newblock Oxford University Press, 1990.

105

50 

1878

51 
\bibitem{paulsonnatural}

105

52 
Lawrence~C. Paulson.


53 
\newblock Natural deduction as higherorder resolution.


54 
\newblock {\em Journal of Logic Programming}, 3:237258, 1986.


55 


56 
\bibitem{paulson87}


57 
Lawrence~C. Paulson.


58 
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.


59 
\newblock Cambridge University Press, 1987.


60 

1878

61 
\bibitem{paulsonfound}

105

62 
Lawrence~C. Paulson.


63 
\newblock The foundation of a generic theorem prover.

359

64 
\newblock {\em Journal of Automated Reasoning}, 5(3):363397, 1989.

105

65 


66 
\bibitem{paulson700}


67 
Lawrence~C. Paulson.


68 
\newblock {Isabelle}: The next 700 theorem provers.


69 
\newblock In P.~Odifreddi, editor, {\em Logic and Computer Science}, pages


70 
361386. Academic Press, 1990.


71 


72 
\bibitem{paulson91}


73 
Lawrence~C. Paulson.


74 
\newblock {\em {ML} for the Working Programmer}.


75 
\newblock Cambridge University Press, 1991.


76 


77 
\bibitem{paulsonhandbook}


78 
Lawrence~C. Paulson.


79 
\newblock Designing a theorem prover.


80 
\newblock In S.~Abramsky, D.~M. Gabbay, and T.~S.~E. Maibaum, editors, {\em


81 
Handbook of Logic in Computer Science}, volume~2, pages 415475. Oxford


82 
University Press, 1992.


83 


84 
\bibitem{pelletier86}


85 
F.~J. Pelletier.


86 
\newblock Seventyfive problems for testing automatic theorem provers.


87 
\newblock {\em Journal of Automated Reasoning}, 2:191216, 1986.

2977

88 
\newblock Errata, JAR 4 (1988), 235236 and JAR 18 (1997), 135.

105

89 


90 
\bibitem{reeves90}


91 
Steve Reeves and Michael Clarke.


92 
\newblock {\em Logic for Computer Science}.


93 
\newblock AddisonWesley, 1990.


94 


95 
\bibitem{suppes72}


96 
Patrick Suppes.


97 
\newblock {\em Axiomatic Set Theory}.


98 
\newblock Dover, 1972.


99 


100 
\bibitem{wosbledsoe}


101 
Larry Wos.


102 
\newblock Automated reasoning and {Bledsoe's} dream for the field.


103 
\newblock In Robert~S. Boyer, editor, {\em Automated Reasoning: Essays in Honor


104 
of {Woody Bledsoe}}, pages 297342. Kluwer Academic Publishers, 1991.


105 


106 
\end{thebibliography}
