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