doc-src/springer.bbl
author paulson
Fri, 17 Jan 1997 12:49:31 +0100
changeset 2516 4d68fbe6378b
parent 460 5d91bd2db00a
permissions -rw-r--r--
Now with Andy Gordon's treatment of freshness to replace newN/K
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
460
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
     1
\begin{thebibliography}{10}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
     2
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
     3
\bibitem{andrews86}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
     4
Andrews, P.~B.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
     5
\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
     6
  Through Proof},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
     7
\newblock Academic Press, 1986
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
     8
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
     9
\bibitem{basin91}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    10
Basin, D., Kaufmann, M.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    11
\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    12
\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    13
  Univ. Press, 1991, pp.~89--119
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    14
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    15
\bibitem{boyer86}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    16
Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    17
\newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    18
\newblock {\em J. Auto. Reas. {\bf 2}}, 3 (1986), 287--327
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    19
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    20
\bibitem{bm88book}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    21
Boyer, R.~S., Moore, J.~S.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    22
\newblock {\em A Computational Logic Handbook},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    23
\newblock Academic Press, 1988
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    24
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    25
\bibitem{camilleri92}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    26
Camilleri, J., Melham, T.~F.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    27
\newblock Reasoning with inductively defined relations in the {HOL} theorem
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    28
  prover,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    29
\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    30
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    31
\bibitem{charniak80}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    32
Charniak, E., Riesbeck, C.~K., McDermott, D.~V.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    33
\newblock {\em Artificial Intelligence Programming},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    34
\newblock Lawrence Erlbaum Associates, 1980
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    35
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    36
\bibitem{church40}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    37
Church, A.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    38
\newblock A formulation of the simple theory of types,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    39
\newblock {\em J. Symb. Logic {\bf 5}\/} (1940), 56--68
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    40
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    41
\bibitem{coen92}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    42
Coen, M.~D.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    43
\newblock {\em Interactive Program Derivation},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    44
\newblock PhD thesis, University of Cambridge, 1992,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    45
\newblock Computer Laboratory Technical Report 272
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    46
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    47
\bibitem{constable86}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    48
{Constable et al.}, R.~L.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    49
\newblock {\em Implementing Mathematics with the Nuprl Proof Development
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    50
  System},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    51
\newblock Prentice-Hall, 1986
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    52
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    53
\bibitem{davey&priestley}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    54
Davey, B.~A., Priestley, H.~A.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    55
\newblock {\em Introduction to Lattices and Order},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    56
\newblock Cambridge Univ. Press, 1990
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    57
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    58
\bibitem{dawson90}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    59
Dawson, W.~M.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    60
\newblock {\em A Generic Logic Environment},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    61
\newblock PhD thesis, Imperial College, London, 1990
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    62
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    63
\bibitem{debruijn72}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    64
de~Bruijn, N.~G.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    65
\newblock Lambda calculus notation with nameless dummies, a tool for automatic
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    66
  formula manipulation, with application to the {Church-Rosser Theorem},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    67
\newblock {\em Indag. Math. {\bf 34}\/} (1972), 381--392
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    68
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    69
\bibitem{devlin79}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    70
Devlin, K.~J.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    71
\newblock {\em Fundamentals of Contemporary Set Theory},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    72
\newblock Springer, 1979
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    73
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    74
\bibitem{coq}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    75
{Dowek et al.}, G.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    76
\newblock The {Coq} proof assistant user's guide,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    77
\newblock Technical Report 134, INRIA-Rocquencourt, 1991
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    78
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    79
\bibitem{dummett}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    80
Dummett, M.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    81
\newblock {\em Elements of Intuitionism},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    82
\newblock Oxford University Press, 1977
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    83
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    84
\bibitem{dyckhoff}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    85
Dyckhoff, R.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    86
\newblock Contraction-free sequent calculi for intuitionistic logic,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    87
\newblock {\em J. Symb. Logic {\bf 57}}, 3 (1992), 795--807
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    88
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    89
\bibitem{felty91a}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    90
Felty, A.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    91
\newblock A logic program for transforming sequent proofs to natural deduction
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    92
  proofs,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    93
\newblock In {\em Extensions of Logic Programming\/} (1991),
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    94
  P.~Schroeder-Heister, Ed., Springer, pp.~157--178,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    95
\newblock LNAI 475
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    96
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    97
\bibitem{felty93}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    98
Felty, A.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
    99
\newblock Implementing tactics and tacticals in a higher-order logic
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   100
  programming language,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   101
\newblock {\em J. Auto. Reas. {\bf 11}}, 1 (1993), 43--82
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   102
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   103
\bibitem{frost93}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   104
Frost, J.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   105
\newblock A case study of co-induction in {Isabelle HOL},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   106
\newblock Tech. Rep. 308, Comp. Lab., Univ. Cambridge, Aug. 1993
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   107
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   108
\bibitem{OBJ}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   109
Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   110
\newblock Principles of {OBJ2},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   111
\newblock In {\em Princ. Prog. Lang.\/} (1985), pp.~52--66
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   112
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   113
\bibitem{gallier86}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   114
Gallier, J.~H.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   115
\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   116
  Proving},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   117
\newblock Harper \& Row, 1986
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   118
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   119
\bibitem{mgordon-hol}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   120
Gordon, M. J.~C., Melham, T.~F.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   121
\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   122
  Order Logic},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   123
\newblock Cambridge Univ. Press, 1993
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   124
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   125
\bibitem{halmos60}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   126
Halmos, P.~R.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   127
\newblock {\em Naive Set Theory},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   128
\newblock Van Nostrand, 1960
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   129
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   130
\bibitem{harper-jacm}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   131
Harper, R., Honsell, F., Plotkin, G.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   132
\newblock A framework for defining logics,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   133
\newblock {\em J.~ACM {\bf 40}}, 1 (1993), 143--184
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   134
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   135
\bibitem{haskell-tutorial}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   136
Hudak, P., Fasel, J.~H.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   137
\newblock A gentle introduction to {Haskell},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   138
\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992)
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   139
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   140
\bibitem{haskell-report}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   141
Hudak, P., Jones, S.~P., Wadler, P.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   142
\newblock Report on the programming language {Haskell}: A non-strict, purely
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   143
  functional language,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   144
\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992),
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   145
\newblock Version 1.2
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   146
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   147
\bibitem{huet75}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   148
Huet, G.~P.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   149
\newblock A unification algorithm for typed $\lambda$-calculus,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   150
\newblock {\em Theoretical Comput. Sci. {\bf 1}\/} (1975), 27--57
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   151
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   152
\bibitem{huet78}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   153
Huet, G.~P., Lang, B.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   154
\newblock Proving and applying program transformations expressed with
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   155
  second-order patterns,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   156
\newblock {\em Acta Inf. {\bf 11}\/} (1978), 31--55
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   157
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   158
\bibitem{mural}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   159
Jones, C.~B., Jones, K.~D., Lindsay, P.~A., Moore, R.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   160
\newblock {\em Mural: A Formal Development Support System},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   161
\newblock Springer, 1991
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   162
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   163
\bibitem{alf}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   164
Magnusson, L., {Nordstr\"om}, B.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   165
\newblock The {ALF} proof editor and its proof engine,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   166
\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   167
  '93}\/} (published 1994), Springer, pp.~213--237,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   168
\newblock LNCS 806
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   169
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   170
\bibitem{mw81}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   171
Manna, Z., Waldinger, R.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   172
\newblock Deductive synthesis of the unification algorithm,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   173
\newblock {\em Sci. Comput. Programming {\bf 1}}, 1 (1981), 5--48
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   174
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   175
\bibitem{martin-nipkow}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   176
Martin, U., Nipkow, T.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   177
\newblock Ordered rewriting and confluence,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   178
\newblock In {\em 10th Conf. Auto. Deduct.\/} (1990), M.~E. Stickel, Ed.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   179
  Springer, pp.~366--380,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   180
\newblock LNCS 449
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   181
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   182
\bibitem{martinlof84}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   183
Martin-L\"of, P.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   184
\newblock {\em Intuitionistic type theory},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   185
\newblock Bibliopolis, 1984
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   186
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   187
\bibitem{melham89}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   188
Melham, T.~F.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   189
\newblock Automating recursive type definitions in higher order logic,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   190
\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   191
  Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   192
  pp.~341--386
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   193
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   194
\bibitem{miller-mixed}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   195
Miller, D.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   196
\newblock Unification under a mixed prefix,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   197
\newblock {\em J. Symb. Comput. {\bf 14}}, 4 (1992), 321--358
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   198
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   199
\bibitem{milner-coind}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   200
Milner, R., Tofte, M.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   201
\newblock Co-induction in relational semantics,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   202
\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   203
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   204
\bibitem{nipkow-prehofer}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   205
Nipkow, T., Prehofer, C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   206
\newblock Type checking type classes,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   207
\newblock In {\em 20th Princ. Prog. Lang.\/} (1993), ACM Press, pp.~409--418,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   208
\newblock Revised version to appear in \bgroup\em J. Func. Prog.\egroup
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   209
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   210
\bibitem{noel}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   211
{No\"el}, P.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   212
\newblock Experimenting with {Isabelle} in {ZF} set theory,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   213
\newblock {\em J. Auto. Reas. {\bf 10}}, 1 (1993), 15--58
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   214
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   215
\bibitem{nordstrom90}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   216
{Nordstr\"om}, B., Petersson, K., Smith, J.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   217
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   218
\newblock Oxford University Press, 1990
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   219
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   220
\bibitem{paulin92}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   221
Paulin-Mohring, C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   222
\newblock Inductive definitions in the system {Coq}: Rules and properties,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   223
\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   224
  1992
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   225
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   226
\bibitem{paulson85}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   227
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   228
\newblock Verifying the unification algorithm in {LCF},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   229
\newblock {\em Sci. Comput. Programming {\bf 5}\/} (1985), 143--170
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   230
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   231
\bibitem{paulson87}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   232
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   233
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   234
\newblock Cambridge Univ. Press, 1987
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   235
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   236
\bibitem{paulson89}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   237
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   238
\newblock The foundation of a generic theorem prover,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   239
\newblock {\em J. Auto. Reas. {\bf 5}}, 3 (1989), 363--397
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   240
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   241
\bibitem{paulson-COLOG}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   242
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   243
\newblock A formulation of the simple theory of types (for {Isabelle}),
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   244
\newblock In {\em COLOG-88: International Conference on Computer Logic\/}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   245
  (Tallinn, 1990), P.~Martin-L\"of, G.~Mints, Eds., Estonian Academy of
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   246
  Sciences, Springer,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   247
\newblock LNCS 417
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   248
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   249
\bibitem{paulson700}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   250
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   251
\newblock {Isabelle}: The next 700 theorem provers,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   252
\newblock In {\em Logic and Computer Science}, P.~Odifreddi, Ed. Academic
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   253
  Press, 1990, pp.~361--386
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   254
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   255
\bibitem{paulson91}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   256
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   257
\newblock {\em {ML} for the Working Programmer},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   258
\newblock Cambridge Univ. Press, 1991
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   259
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   260
\bibitem{paulson-coind}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   261
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   262
\newblock Co-induction and co-recursion in higher-order logic,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   263
\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   264
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   265
\bibitem{paulson-fixedpt}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   266
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   267
\newblock A fixedpoint approach to implementing (co)inductive definitions,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   268
\newblock Tech. Rep. 320, Comp. Lab., Univ. Cambridge, Dec. 1993
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   269
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   270
\bibitem{paulson-set-I}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   271
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   272
\newblock Set theory for verification: {I}. {From} foundations to functions,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   273
\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   274
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   275
\bibitem{paulson-set-II}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   276
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   277
\newblock Set theory for verification: {II}. {Induction} and recursion,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   278
\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   279
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   280
\bibitem{paulson-final}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   281
Paulson, L.~C.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   282
\newblock A concrete final coalgebra theorem for {ZF} set theory,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   283
\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   284
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   285
\bibitem{pelletier86}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   286
Pelletier, F.~J.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   287
\newblock Seventy-five problems for testing automatic theorem provers,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   288
\newblock {\em J. Auto. Reas. {\bf 2}\/} (1986), 191--216,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   289
\newblock Errata, JAR 4 (1988), 235--236
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   290
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   291
\bibitem{plaisted90}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   292
Plaisted, D.~A.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   293
\newblock A sequent-style model elimination strategy and a positive refinement,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   294
\newblock {\em J. Auto. Reas. {\bf 6}}, 4 (1990), 389--402
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   295
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   296
\bibitem{quaife92}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   297
Quaife, A.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   298
\newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   299
\newblock {\em J. Auto. Reas. {\bf 8}}, 1 (1992), 91--147
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   300
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   301
\bibitem{sawamura92}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   302
Sawamura, H., Minami, T., Ohashi, K.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   303
\newblock Proof methods based on sheet of thought in {EUODHILOS},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   304
\newblock Research Report IIAS-RR-92-6E, International Institute for Advanced
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   305
  Study of Social Information Science, Fujitsu Laboratories, 1992
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   306
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   307
\bibitem{suppes72}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   308
Suppes, P.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   309
\newblock {\em Axiomatic Set Theory},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   310
\newblock Dover, 1972
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   311
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   312
\bibitem{takeuti87}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   313
Takeuti, G.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   314
\newblock {\em Proof Theory}, 2nd~ed.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   315
\newblock North Holland, 1987
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   316
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   317
\bibitem{thompson91}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   318
Thompson, S.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   319
\newblock {\em Type Theory and Functional Programming},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   320
\newblock Addison-Wesley, 1991
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   321
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   322
\bibitem{principia}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   323
Whitehead, A.~N., Russell, B.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   324
\newblock {\em Principia Mathematica},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   325
\newblock Cambridge Univ. Press, 1962,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   326
\newblock Paperback edition to *56, abridged from the 2nd edition (1927)
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   327
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   328
\bibitem{wos-bledsoe}
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   329
Wos, L.,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   330
\newblock Automated reasoning and {Bledsoe's} dream for the field,
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   331
\newblock In {\em Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   332
  R.~S. Boyer, Ed. Kluwer Academic Publishers, 1991, pp.~297--342
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   333
5d91bd2db00a restoring after deletion
lcp
parents:
diff changeset
   334
\end{thebibliography}