doc-src/Ref/ref.bbl
author paulson
Fri, 27 Nov 1998 13:13:22 +0100
changeset 5980 2e9314c07146
parent 3088 857c1c05f0c7
child 6592 c120262044b6
permissions -rw-r--r--
added Real/Hyperreal
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
730
15c822377c18 new reference to HO patterns
lcp
parents: 359
diff changeset
     1
\begin{thebibliography}{10}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
359
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
     3
\bibitem{bm88book}
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
     4
Robert~S. Boyer and J~Strother Moore.
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
     5
\newblock {\em A Computational Logic Handbook}.
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
     6
\newblock Academic Press, 1988.
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
     7
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
\bibitem{charniak80}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
E.~Charniak, C.~K. Riesbeck, and D.~V. McDermott.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
\newblock {\em Artificial Intelligence Programming}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
\newblock Lawrence Erlbaum Associates, 1980.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
\bibitem{debruijn72}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
N.~G. de~Bruijn.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
\newblock Lambda calculus notation with nameless dummies, a tool for automatic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
  formula manipulation, with application to the {Church-Rosser Theorem}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
\newblock {\em Indagationes Mathematicae}, 34:381--392, 1972.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
359
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    19
\bibitem{OBJ}
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    20
K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer.
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    21
\newblock Principles of {OBJ2}.
1255
0e76adc74e7f trivial update to POPL title
paulson
parents: 1224
diff changeset
    22
\newblock In {\em Symposium on Principles of Programming Languages}, pages
0e76adc74e7f trivial update to POPL title
paulson
parents: 1224
diff changeset
    23
  52--66, 1985.
359
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    24
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    25
\bibitem{martin-nipkow}
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    26
Ursula Martin and Tobias Nipkow.
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    27
\newblock Ordered rewriting and confluence.
878
7c82ab7602b4 changed due to new .bib files
lcp
parents: 730
diff changeset
    28
\newblock In Mark~E. Stickel, editor, {\em 10th International Conference on
1399
1f00494e37a5 trivial, automatic changes
paulson
parents: 1255
diff changeset
    29
  Automated Deduction}, LNAI 449, pages 366--380. Springer, 1990.
359
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    30
2020
586f3c075b05 Restoration of reference to Nipkow, LICS, 1993
paulson
parents: 2008
diff changeset
    31
\bibitem{nipkow-patterns}
586f3c075b05 Restoration of reference to Nipkow, LICS, 1993
paulson
parents: 2008
diff changeset
    32
Tobias Nipkow.
586f3c075b05 Restoration of reference to Nipkow, LICS, 1993
paulson
parents: 2008
diff changeset
    33
\newblock Functional unification of higher-order patterns.
586f3c075b05 Restoration of reference to Nipkow, LICS, 1993
paulson
parents: 2008
diff changeset
    34
\newblock In M.~Vardi, editor, {\em Eighth Annual Symposium on Logic in
586f3c075b05 Restoration of reference to Nipkow, LICS, 1993
paulson
parents: 2008
diff changeset
    35
  Computer Science}, pages 64--74. {\sc ieee} Computer Society Press, 1993.
586f3c075b05 Restoration of reference to Nipkow, LICS, 1993
paulson
parents: 2008
diff changeset
    36
178
afbb13cb34ca new references
lcp
parents: 104
diff changeset
    37
\bibitem{nipkow-prehofer}
afbb13cb34ca new references
lcp
parents: 104
diff changeset
    38
Tobias Nipkow and Christian Prehofer.
1182
30286ceb9adb Updated nipkow-prehofer
nipkow
parents: 878
diff changeset
    39
\newblock Type reconstruction for type classes.
1224
3d739c8e2536 Trivial reformatting of reference
paulson
parents: 1182
diff changeset
    40
\newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995.
359
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    41
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    42
\bibitem{nordstrom90}
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    43
Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    44
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
b5a2e9503a7a final Springer version
lcp
parents: 178
diff changeset
    45
\newblock Oxford University Press, 1990.
178
afbb13cb34ca new references
lcp
parents: 104
diff changeset
    46
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
\bibitem{paulson91}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
Lawrence~C. Paulson.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
\newblock {\em {ML} for the Working Programmer}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
\newblock Cambridge University Press, 1991.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
1848
e251196383cd Added ML reference
paulson
parents: 1399
diff changeset
    52
\bibitem{paulson-ml2}
e251196383cd Added ML reference
paulson
parents: 1399
diff changeset
    53
Lawrence~C. Paulson.
e251196383cd Added ML reference
paulson
parents: 1399
diff changeset
    54
\newblock {\em {ML} for the Working Programmer}.
e251196383cd Added ML reference
paulson
parents: 1399
diff changeset
    55
\newblock Cambridge University Press, 2nd edition, 1996.
e251196383cd Added ML reference
paulson
parents: 1399
diff changeset
    56
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
\bibitem{pelletier86}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
F.~J. Pelletier.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
\newblock Seventy-five problems for testing automatic theorem provers.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
3088
857c1c05f0c7 Automatic update
paulson
parents: 2020
diff changeset
    61
\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
\end{thebibliography}