730
|
1 |
\begin{thebibliography}{10}
|
104
|
2 |
|
359
|
3 |
\bibitem{bm88book}
|
|
4 |
Robert~S. Boyer and J~Strother Moore.
|
|
5 |
\newblock {\em A Computational Logic Handbook}.
|
|
6 |
\newblock Academic Press, 1988.
|
|
7 |
|
104
|
8 |
\bibitem{charniak80}
|
|
9 |
E.~Charniak, C.~K. Riesbeck, and D.~V. McDermott.
|
|
10 |
\newblock {\em Artificial Intelligence Programming}.
|
|
11 |
\newblock Lawrence Erlbaum Associates, 1980.
|
|
12 |
|
|
13 |
\bibitem{debruijn72}
|
|
14 |
N.~G. de~Bruijn.
|
|
15 |
\newblock Lambda calculus notation with nameless dummies, a tool for automatic
|
|
16 |
formula manipulation, with application to the {Church-Rosser Theorem}.
|
|
17 |
\newblock {\em Indagationes Mathematicae}, 34:381--392, 1972.
|
|
18 |
|
359
|
19 |
\bibitem{OBJ}
|
|
20 |
K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer.
|
|
21 |
\newblock Principles of {OBJ2}.
|
1255
|
22 |
\newblock In {\em Symposium on Principles of Programming Languages}, pages
|
|
23 |
52--66, 1985.
|
359
|
24 |
|
|
25 |
\bibitem{martin-nipkow}
|
|
26 |
Ursula Martin and Tobias Nipkow.
|
|
27 |
\newblock Ordered rewriting and confluence.
|
878
|
28 |
\newblock In Mark~E. Stickel, editor, {\em 10th International Conference on
|
1399
|
29 |
Automated Deduction}, LNAI 449, pages 366--380. Springer, 1990.
|
359
|
30 |
|
2020
|
31 |
\bibitem{nipkow-patterns}
|
|
32 |
Tobias Nipkow.
|
|
33 |
\newblock Functional unification of higher-order patterns.
|
|
34 |
\newblock In M.~Vardi, editor, {\em Eighth Annual Symposium on Logic in
|
|
35 |
Computer Science}, pages 64--74. {\sc ieee} Computer Society Press, 1993.
|
|
36 |
|
178
|
37 |
\bibitem{nipkow-prehofer}
|
|
38 |
Tobias Nipkow and Christian Prehofer.
|
1182
|
39 |
\newblock Type reconstruction for type classes.
|
1224
|
40 |
\newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995.
|
359
|
41 |
|
|
42 |
\bibitem{nordstrom90}
|
|
43 |
Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
|
|
44 |
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
|
|
45 |
\newblock Oxford University Press, 1990.
|
178
|
46 |
|
104
|
47 |
\bibitem{paulson91}
|
|
48 |
Lawrence~C. Paulson.
|
|
49 |
\newblock {\em {ML} for the Working Programmer}.
|
|
50 |
\newblock Cambridge University Press, 1991.
|
|
51 |
|
1848
|
52 |
\bibitem{paulson-ml2}
|
|
53 |
Lawrence~C. Paulson.
|
|
54 |
\newblock {\em {ML} for the Working Programmer}.
|
|
55 |
\newblock Cambridge University Press, 2nd edition, 1996.
|
|
56 |
|
104
|
57 |
\bibitem{pelletier86}
|
|
58 |
F.~J. Pelletier.
|
|
59 |
\newblock Seventy-five problems for testing automatic theorem provers.
|
|
60 |
\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
|
3088
|
61 |
\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
|
104
|
62 |
|
|
63 |
\end{thebibliography}
|