author | paulson |
Fri, 22 Dec 1995 10:19:55 +0100 | |
changeset 1412 | 2ab32768c996 |
parent 1399 | 1f00494e37a5 |
child 1848 | e251196383cd |
permissions | -rw-r--r-- |
\begin{thebibliography}{10} \bibitem{bm88book} Robert~S. Boyer and J~Strother Moore. \newblock {\em A Computational Logic Handbook}. \newblock Academic Press, 1988. \bibitem{charniak80} E.~Charniak, C.~K. Riesbeck, and D.~V. McDermott. \newblock {\em Artificial Intelligence Programming}. \newblock Lawrence Erlbaum Associates, 1980. \bibitem{debruijn72} N.~G. de~Bruijn. \newblock Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the {Church-Rosser Theorem}. \newblock {\em Indagationes Mathematicae}, 34:381--392, 1972. \bibitem{OBJ} K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer. \newblock Principles of {OBJ2}. \newblock In {\em Symposium on Principles of Programming Languages}, pages 52--66, 1985. \bibitem{martin-nipkow} Ursula Martin and Tobias Nipkow. \newblock Ordered rewriting and confluence. \newblock In Mark~E. Stickel, editor, {\em 10th International Conference on Automated Deduction}, LNAI 449, pages 366--380. Springer, 1990. \bibitem{Nipkow-LICS-93} Tobias Nipkow. \newblock Functional unification of higher-order patterns. \newblock In M.~Vardi, editor, {\em Eighth Annual Symposium on Logic in Computer Science}, pages 64--74. {\sc ieee} Computer Society Press, 1993. \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{paulson91} Lawrence~C. Paulson. \newblock {\em {ML} for the Working Programmer}. \newblock Cambridge University Press, 1991. \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. \end{thebibliography}