doc-src/Intro/intro.bbl
author wenzelm
Thu, 17 Jul 1997 15:03:38 +0200
changeset 3524 c02cb15830de
parent 2977 6c035c126d7f
child 6592 c120262044b6
permissions -rw-r--r--
fixed EqI meta rule;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     1
\begin{thebibliography}{10}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     2
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     3
\bibitem{galton90}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     4
Antony Galton.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     5
\newblock {\em Logic for Information Technology}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     6
\newblock Wiley, 1990.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     7
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
     8
\bibitem{mgordon-hol}
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
     9
M.~J.~C. Gordon and T.~F. Melham.
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    10
\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    11
  Order Logic}.
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    12
\newblock Cambridge University Press, 1993.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    13
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    14
\bibitem{mgordon79}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    15
Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    16
\newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}.
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1224
diff changeset
    17
\newblock LNCS 78. Springer, 1979.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    18
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    19
\bibitem{haskell-tutorial}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    20
Paul Hudak and Joseph~H. Fasel.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    21
\newblock A gentle introduction to {Haskell}.
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    22
\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    23
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    24
\bibitem{haskell-report}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    25
Paul Hudak, Simon~Peyton Jones, and Philip Wadler.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    26
\newblock Report on the programming language {Haskell}: A non-strict, purely
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    27
  functional language.
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    28
\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    29
\newblock Version 1.2.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    30
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    31
\bibitem{huet75}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    32
G.~P. Huet.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    33
\newblock A unification algorithm for typed $\lambda$-calculus.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    34
\newblock {\em Theoretical Computer Science}, 1:27--57, 1975.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    35
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    36
\bibitem{miller-mixed}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    37
Dale Miller.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    38
\newblock Unification under a mixed prefix.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    39
\newblock {\em Journal of Symbolic Computation}, 14(4):321--358, 1992.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    40
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    41
\bibitem{nipkow-prehofer}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    42
Tobias Nipkow and Christian Prehofer.
1182
30286ceb9adb Updated nipkow-prehofer
nipkow
parents: 359
diff changeset
    43
\newblock Type reconstruction for type classes.
1224
3d739c8e2536 Trivial reformatting of reference
paulson
parents: 1182
diff changeset
    44
\newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    45
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    46
\bibitem{nordstrom90}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    47
Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    48
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    49
\newblock Oxford University Press, 1990.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    50
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1224
diff changeset
    51
\bibitem{paulson-natural}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    52
Lawrence~C. Paulson.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    53
\newblock Natural deduction as higher-order resolution.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    54
\newblock {\em Journal of Logic Programming}, 3:237--258, 1986.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    55
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    56
\bibitem{paulson87}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    57
Lawrence~C. Paulson.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    58
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    59
\newblock Cambridge University Press, 1987.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    60
1878
ac8e534b4834 Updated BibTeX identifiers
paulson
parents: 1224
diff changeset
    61
\bibitem{paulson-found}
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    62
Lawrence~C. Paulson.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    63
\newblock The foundation of a generic theorem prover.
359
b5a2e9503a7a final Springer version
lcp
parents: 105
diff changeset
    64
\newblock {\em Journal of Automated Reasoning}, 5(3):363--397, 1989.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    65
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    66
\bibitem{paulson700}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    67
Lawrence~C. Paulson.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    68
\newblock {Isabelle}: The next 700 theorem provers.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    69
\newblock In P.~Odifreddi, editor, {\em Logic and Computer Science}, pages
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    70
  361--386. Academic Press, 1990.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    71
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    72
\bibitem{paulson91}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    73
Lawrence~C. Paulson.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    74
\newblock {\em {ML} for the Working Programmer}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    75
\newblock Cambridge University Press, 1991.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    76
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    77
\bibitem{paulson-handbook}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    78
Lawrence~C. Paulson.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    79
\newblock Designing a theorem prover.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    80
\newblock In S.~Abramsky, D.~M. Gabbay, and T.~S.~E. Maibaum, editors, {\em
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    81
  Handbook of Logic in Computer Science}, volume~2, pages 415--475. Oxford
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    82
  University Press, 1992.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    83
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    84
\bibitem{pelletier86}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    85
F.~J. Pelletier.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    86
\newblock Seventy-five problems for testing automatic theorem provers.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    87
\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
2977
6c035c126d7f Automatic updates
paulson
parents: 1878
diff changeset
    88
\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    89
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    90
\bibitem{reeves90}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    91
Steve Reeves and Michael Clarke.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    92
\newblock {\em Logic for Computer Science}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    93
\newblock Addison-Wesley, 1990.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    94
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    95
\bibitem{suppes72}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    96
Patrick Suppes.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    97
\newblock {\em Axiomatic Set Theory}.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    98
\newblock Dover, 1972.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    99
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   100
\bibitem{wos-bledsoe}
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   101
Larry Wos.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   102
\newblock Automated reasoning and {Bledsoe's} dream for the field.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   103
\newblock In Robert~S. Boyer, editor, {\em Automated Reasoning: Essays in Honor
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   104
  of {Woody Bledsoe}}, pages 297--342. Kluwer Academic Publishers, 1991.
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   106
\end{thebibliography}