5375
|
1 |
\begin{thebibliography}{1}
|
|
2 |
|
|
3 |
\bibitem{Bird-Wadler}
|
|
4 |
Richard Bird and Philip Wadler.
|
|
5 |
\newblock {\em Introduction to Functional Programming}.
|
|
6 |
\newblock Prentice-Hall, 1988.
|
|
7 |
|
5850
|
8 |
\bibitem{Gunter-HOL92}
|
|
9 |
Elsa~L. Gunter.
|
|
10 |
\newblock Why we can't have {SML} style datatype declarations in {HOL}.
|
|
11 |
\newblock In L.J.M. Claesen and M.J.C. Gordon, editors, {\em Higher Order Logic
|
|
12 |
Theorem Proving and its Applications: Proc.\ IFIP TC10/WG10.2 Intl. Workshop,
|
|
13 |
1992}, pages 561--568. North-Holland, 1993.
|
|
14 |
|
|
15 |
\bibitem{Knuth3-75}
|
|
16 |
Donald~E. Knuth.
|
|
17 |
\newblock {\em The Art of Computer Programming, Volume 3: Sorting and
|
|
18 |
Searching}.
|
|
19 |
\newblock Addison-Wesley, 1975.
|
|
20 |
|
|
21 |
\bibitem{MuellerNvOS98}
|
|
22 |
Olaf M\"uller, Tobias Nipkow, David~von Oheimb, and Oskar Slotosch.
|
|
23 |
\newblock {HOLCF = HOL + LCF}.
|
6577
|
24 |
\newblock {\em J. Functional Programming}, 1999.
|
|
25 |
\newblock To appear.
|
5850
|
26 |
|
5375
|
27 |
\bibitem{Isa-Ref-Man}
|
|
28 |
Lawrence~C. Paulson.
|
|
29 |
\newblock {\em The Isabelle Reference Manual}.
|
|
30 |
\newblock University of Cambridge, Computer Laboratory.
|
|
31 |
\newblock \verb$http://www.in.tum.de/~isabelle/dist/$.
|
|
32 |
|
|
33 |
\bibitem{Isa-Logics-Man}
|
|
34 |
Lawrence~C. Paulson.
|
|
35 |
\newblock {\em Isabelle's Object-Logics}.
|
|
36 |
\newblock University of Cambridge, Computer Laboratory.
|
|
37 |
\newblock \verb$http://www.in.tum.de/~isabelle/dist/$.
|
|
38 |
|
5850
|
39 |
\bibitem{Paulson-LCF}
|
|
40 |
Lawrence~C. Paulson.
|
|
41 |
\newblock {\em Logic and Computation}.
|
|
42 |
\newblock Cambridge University Press, 1987.
|
|
43 |
|
5375
|
44 |
\bibitem{Paulson-ML}
|
|
45 |
Lawrence~C. Paulson.
|
|
46 |
\newblock {\em ML for the Working Programmer}.
|
|
47 |
\newblock Cambridge University Press, 2nd edition, 1996.
|
|
48 |
|
|
49 |
\end{thebibliography}
|