1 \begin{thebibliography}{10} |
|
2 |
|
3 \bibitem{bm88book} |
|
4 Robert~S. Boyer and J~Strother Moore. |
|
5 \newblock {\em A Computational Logic Handbook}. |
|
6 \newblock Academic Press, 1988. |
|
7 |
|
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 |
|
19 \bibitem{OBJ} |
|
20 K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer. |
|
21 \newblock Principles of {OBJ2}. |
|
22 \newblock In {\em Symposium on Principles of Programming Languages}, pages |
|
23 52--66, 1985. |
|
24 |
|
25 \bibitem{martin-nipkow} |
|
26 Ursula Martin and Tobias Nipkow. |
|
27 \newblock Ordered rewriting and confluence. |
|
28 \newblock In Mark~E. Stickel, editor, {\em 10th International Conference on |
|
29 Automated Deduction}, LNAI 449, pages 366--380. Springer, 1990. |
|
30 |
|
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 |
|
37 \bibitem{nipkow-prehofer} |
|
38 Tobias Nipkow and Christian Prehofer. |
|
39 \newblock Type reconstruction for type classes. |
|
40 \newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995. |
|
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. |
|
46 |
|
47 \bibitem{paulson-ml2} |
|
48 Lawrence~C. Paulson. |
|
49 \newblock {\em {ML} for the Working Programmer}. |
|
50 \newblock Cambridge University Press, 2nd edition, 1996. |
|
51 |
|
52 \bibitem{pelletier86} |
|
53 F.~J. Pelletier. |
|
54 \newblock Seventy-five problems for testing automatic theorem provers. |
|
55 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986. |
|
56 \newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135. |
|
57 |
|
58 \end{thebibliography} |
|