restoring after deletion
authorlcp
Mon Jul 11 18:33:28 1994 +0200 (1994-07-11)
changeset 4605d91bd2db00a
parent 459 03b445551763
child 461 170de0c52a9b
restoring after deletion
doc-src/springer.bbl
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/springer.bbl	Mon Jul 11 18:33:28 1994 +0200
     1.3 @@ -0,0 +1,334 @@
     1.4 +\begin{thebibliography}{10}
     1.5 +
     1.6 +\bibitem{andrews86}
     1.7 +Andrews, P.~B.,
     1.8 +\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
     1.9 +  Through Proof},
    1.10 +\newblock Academic Press, 1986
    1.11 +
    1.12 +\bibitem{basin91}
    1.13 +Basin, D., Kaufmann, M.,
    1.14 +\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison,
    1.15 +\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
    1.16 +  Univ. Press, 1991, pp.~89--119
    1.17 +
    1.18 +\bibitem{boyer86}
    1.19 +Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.,
    1.20 +\newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms,
    1.21 +\newblock {\em J. Auto. Reas. {\bf 2}}, 3 (1986), 287--327
    1.22 +
    1.23 +\bibitem{bm88book}
    1.24 +Boyer, R.~S., Moore, J.~S.,
    1.25 +\newblock {\em A Computational Logic Handbook},
    1.26 +\newblock Academic Press, 1988
    1.27 +
    1.28 +\bibitem{camilleri92}
    1.29 +Camilleri, J., Melham, T.~F.,
    1.30 +\newblock Reasoning with inductively defined relations in the {HOL} theorem
    1.31 +  prover,
    1.32 +\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
    1.33 +
    1.34 +\bibitem{charniak80}
    1.35 +Charniak, E., Riesbeck, C.~K., McDermott, D.~V.,
    1.36 +\newblock {\em Artificial Intelligence Programming},
    1.37 +\newblock Lawrence Erlbaum Associates, 1980
    1.38 +
    1.39 +\bibitem{church40}
    1.40 +Church, A.,
    1.41 +\newblock A formulation of the simple theory of types,
    1.42 +\newblock {\em J. Symb. Logic {\bf 5}\/} (1940), 56--68
    1.43 +
    1.44 +\bibitem{coen92}
    1.45 +Coen, M.~D.,
    1.46 +\newblock {\em Interactive Program Derivation},
    1.47 +\newblock PhD thesis, University of Cambridge, 1992,
    1.48 +\newblock Computer Laboratory Technical Report 272
    1.49 +
    1.50 +\bibitem{constable86}
    1.51 +{Constable et al.}, R.~L.,
    1.52 +\newblock {\em Implementing Mathematics with the Nuprl Proof Development
    1.53 +  System},
    1.54 +\newblock Prentice-Hall, 1986
    1.55 +
    1.56 +\bibitem{davey&priestley}
    1.57 +Davey, B.~A., Priestley, H.~A.,
    1.58 +\newblock {\em Introduction to Lattices and Order},
    1.59 +\newblock Cambridge Univ. Press, 1990
    1.60 +
    1.61 +\bibitem{dawson90}
    1.62 +Dawson, W.~M.,
    1.63 +\newblock {\em A Generic Logic Environment},
    1.64 +\newblock PhD thesis, Imperial College, London, 1990
    1.65 +
    1.66 +\bibitem{debruijn72}
    1.67 +de~Bruijn, N.~G.,
    1.68 +\newblock Lambda calculus notation with nameless dummies, a tool for automatic
    1.69 +  formula manipulation, with application to the {Church-Rosser Theorem},
    1.70 +\newblock {\em Indag. Math. {\bf 34}\/} (1972), 381--392
    1.71 +
    1.72 +\bibitem{devlin79}
    1.73 +Devlin, K.~J.,
    1.74 +\newblock {\em Fundamentals of Contemporary Set Theory},
    1.75 +\newblock Springer, 1979
    1.76 +
    1.77 +\bibitem{coq}
    1.78 +{Dowek et al.}, G.,
    1.79 +\newblock The {Coq} proof assistant user's guide,
    1.80 +\newblock Technical Report 134, INRIA-Rocquencourt, 1991
    1.81 +
    1.82 +\bibitem{dummett}
    1.83 +Dummett, M.,
    1.84 +\newblock {\em Elements of Intuitionism},
    1.85 +\newblock Oxford University Press, 1977
    1.86 +
    1.87 +\bibitem{dyckhoff}
    1.88 +Dyckhoff, R.,
    1.89 +\newblock Contraction-free sequent calculi for intuitionistic logic,
    1.90 +\newblock {\em J. Symb. Logic {\bf 57}}, 3 (1992), 795--807
    1.91 +
    1.92 +\bibitem{felty91a}
    1.93 +Felty, A.,
    1.94 +\newblock A logic program for transforming sequent proofs to natural deduction
    1.95 +  proofs,
    1.96 +\newblock In {\em Extensions of Logic Programming\/} (1991),
    1.97 +  P.~Schroeder-Heister, Ed., Springer, pp.~157--178,
    1.98 +\newblock LNAI 475
    1.99 +
   1.100 +\bibitem{felty93}
   1.101 +Felty, A.,
   1.102 +\newblock Implementing tactics and tacticals in a higher-order logic
   1.103 +  programming language,
   1.104 +\newblock {\em J. Auto. Reas. {\bf 11}}, 1 (1993), 43--82
   1.105 +
   1.106 +\bibitem{frost93}
   1.107 +Frost, J.,
   1.108 +\newblock A case study of co-induction in {Isabelle HOL},
   1.109 +\newblock Tech. Rep. 308, Comp. Lab., Univ. Cambridge, Aug. 1993
   1.110 +
   1.111 +\bibitem{OBJ}
   1.112 +Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.,
   1.113 +\newblock Principles of {OBJ2},
   1.114 +\newblock In {\em Princ. Prog. Lang.\/} (1985), pp.~52--66
   1.115 +
   1.116 +\bibitem{gallier86}
   1.117 +Gallier, J.~H.,
   1.118 +\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
   1.119 +  Proving},
   1.120 +\newblock Harper \& Row, 1986
   1.121 +
   1.122 +\bibitem{mgordon-hol}
   1.123 +Gordon, M. J.~C., Melham, T.~F.,
   1.124 +\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
   1.125 +  Order Logic},
   1.126 +\newblock Cambridge Univ. Press, 1993
   1.127 +
   1.128 +\bibitem{halmos60}
   1.129 +Halmos, P.~R.,
   1.130 +\newblock {\em Naive Set Theory},
   1.131 +\newblock Van Nostrand, 1960
   1.132 +
   1.133 +\bibitem{harper-jacm}
   1.134 +Harper, R., Honsell, F., Plotkin, G.,
   1.135 +\newblock A framework for defining logics,
   1.136 +\newblock {\em J.~ACM {\bf 40}}, 1 (1993), 143--184
   1.137 +
   1.138 +\bibitem{haskell-tutorial}
   1.139 +Hudak, P., Fasel, J.~H.,
   1.140 +\newblock A gentle introduction to {Haskell},
   1.141 +\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992)
   1.142 +
   1.143 +\bibitem{haskell-report}
   1.144 +Hudak, P., Jones, S.~P., Wadler, P.,
   1.145 +\newblock Report on the programming language {Haskell}: A non-strict, purely
   1.146 +  functional language,
   1.147 +\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992),
   1.148 +\newblock Version 1.2
   1.149 +
   1.150 +\bibitem{huet75}
   1.151 +Huet, G.~P.,
   1.152 +\newblock A unification algorithm for typed $\lambda$-calculus,
   1.153 +\newblock {\em Theoretical Comput. Sci. {\bf 1}\/} (1975), 27--57
   1.154 +
   1.155 +\bibitem{huet78}
   1.156 +Huet, G.~P., Lang, B.,
   1.157 +\newblock Proving and applying program transformations expressed with
   1.158 +  second-order patterns,
   1.159 +\newblock {\em Acta Inf. {\bf 11}\/} (1978), 31--55
   1.160 +
   1.161 +\bibitem{mural}
   1.162 +Jones, C.~B., Jones, K.~D., Lindsay, P.~A., Moore, R.,
   1.163 +\newblock {\em Mural: A Formal Development Support System},
   1.164 +\newblock Springer, 1991
   1.165 +
   1.166 +\bibitem{alf}
   1.167 +Magnusson, L., {Nordstr\"om}, B.,
   1.168 +\newblock The {ALF} proof editor and its proof engine,
   1.169 +\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
   1.170 +  '93}\/} (published 1994), Springer, pp.~213--237,
   1.171 +\newblock LNCS 806
   1.172 +
   1.173 +\bibitem{mw81}
   1.174 +Manna, Z., Waldinger, R.,
   1.175 +\newblock Deductive synthesis of the unification algorithm,
   1.176 +\newblock {\em Sci. Comput. Programming {\bf 1}}, 1 (1981), 5--48
   1.177 +
   1.178 +\bibitem{martin-nipkow}
   1.179 +Martin, U., Nipkow, T.,
   1.180 +\newblock Ordered rewriting and confluence,
   1.181 +\newblock In {\em 10th Conf. Auto. Deduct.\/} (1990), M.~E. Stickel, Ed.,
   1.182 +  Springer, pp.~366--380,
   1.183 +\newblock LNCS 449
   1.184 +
   1.185 +\bibitem{martinlof84}
   1.186 +Martin-L\"of, P.,
   1.187 +\newblock {\em Intuitionistic type theory},
   1.188 +\newblock Bibliopolis, 1984
   1.189 +
   1.190 +\bibitem{melham89}
   1.191 +Melham, T.~F.,
   1.192 +\newblock Automating recursive type definitions in higher order logic,
   1.193 +\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
   1.194 +  Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
   1.195 +  pp.~341--386
   1.196 +
   1.197 +\bibitem{miller-mixed}
   1.198 +Miller, D.,
   1.199 +\newblock Unification under a mixed prefix,
   1.200 +\newblock {\em J. Symb. Comput. {\bf 14}}, 4 (1992), 321--358
   1.201 +
   1.202 +\bibitem{milner-coind}
   1.203 +Milner, R., Tofte, M.,
   1.204 +\newblock Co-induction in relational semantics,
   1.205 +\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
   1.206 +
   1.207 +\bibitem{nipkow-prehofer}
   1.208 +Nipkow, T., Prehofer, C.,
   1.209 +\newblock Type checking type classes,
   1.210 +\newblock In {\em 20th Princ. Prog. Lang.\/} (1993), ACM Press, pp.~409--418,
   1.211 +\newblock Revised version to appear in \bgroup\em J. Func. Prog.\egroup
   1.212 +
   1.213 +\bibitem{noel}
   1.214 +{No\"el}, P.,
   1.215 +\newblock Experimenting with {Isabelle} in {ZF} set theory,
   1.216 +\newblock {\em J. Auto. Reas. {\bf 10}}, 1 (1993), 15--58
   1.217 +
   1.218 +\bibitem{nordstrom90}
   1.219 +{Nordstr\"om}, B., Petersson, K., Smith, J.,
   1.220 +\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction},
   1.221 +\newblock Oxford University Press, 1990
   1.222 +
   1.223 +\bibitem{paulin92}
   1.224 +Paulin-Mohring, C.,
   1.225 +\newblock Inductive definitions in the system {Coq}: Rules and properties,
   1.226 +\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
   1.227 +  1992
   1.228 +
   1.229 +\bibitem{paulson85}
   1.230 +Paulson, L.~C.,
   1.231 +\newblock Verifying the unification algorithm in {LCF},
   1.232 +\newblock {\em Sci. Comput. Programming {\bf 5}\/} (1985), 143--170
   1.233 +
   1.234 +\bibitem{paulson87}
   1.235 +Paulson, L.~C.,
   1.236 +\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
   1.237 +\newblock Cambridge Univ. Press, 1987
   1.238 +
   1.239 +\bibitem{paulson89}
   1.240 +Paulson, L.~C.,
   1.241 +\newblock The foundation of a generic theorem prover,
   1.242 +\newblock {\em J. Auto. Reas. {\bf 5}}, 3 (1989), 363--397
   1.243 +
   1.244 +\bibitem{paulson-COLOG}
   1.245 +Paulson, L.~C.,
   1.246 +\newblock A formulation of the simple theory of types (for {Isabelle}),
   1.247 +\newblock In {\em COLOG-88: International Conference on Computer Logic\/}
   1.248 +  (Tallinn, 1990), P.~Martin-L\"of, G.~Mints, Eds., Estonian Academy of
   1.249 +  Sciences, Springer,
   1.250 +\newblock LNCS 417
   1.251 +
   1.252 +\bibitem{paulson700}
   1.253 +Paulson, L.~C.,
   1.254 +\newblock {Isabelle}: The next 700 theorem provers,
   1.255 +\newblock In {\em Logic and Computer Science}, P.~Odifreddi, Ed. Academic
   1.256 +  Press, 1990, pp.~361--386
   1.257 +
   1.258 +\bibitem{paulson91}
   1.259 +Paulson, L.~C.,
   1.260 +\newblock {\em {ML} for the Working Programmer},
   1.261 +\newblock Cambridge Univ. Press, 1991
   1.262 +
   1.263 +\bibitem{paulson-coind}
   1.264 +Paulson, L.~C.,
   1.265 +\newblock Co-induction and co-recursion in higher-order logic,
   1.266 +\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
   1.267 +
   1.268 +\bibitem{paulson-fixedpt}
   1.269 +Paulson, L.~C.,
   1.270 +\newblock A fixedpoint approach to implementing (co)inductive definitions,
   1.271 +\newblock Tech. Rep. 320, Comp. Lab., Univ. Cambridge, Dec. 1993
   1.272 +
   1.273 +\bibitem{paulson-set-I}
   1.274 +Paulson, L.~C.,
   1.275 +\newblock Set theory for verification: {I}. {From} foundations to functions,
   1.276 +\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
   1.277 +
   1.278 +\bibitem{paulson-set-II}
   1.279 +Paulson, L.~C.,
   1.280 +\newblock Set theory for verification: {II}. {Induction} and recursion,
   1.281 +\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
   1.282 +
   1.283 +\bibitem{paulson-final}
   1.284 +Paulson, L.~C.,
   1.285 +\newblock A concrete final coalgebra theorem for {ZF} set theory,
   1.286 +\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994
   1.287 +
   1.288 +\bibitem{pelletier86}
   1.289 +Pelletier, F.~J.,
   1.290 +\newblock Seventy-five problems for testing automatic theorem provers,
   1.291 +\newblock {\em J. Auto. Reas. {\bf 2}\/} (1986), 191--216,
   1.292 +\newblock Errata, JAR 4 (1988), 235--236
   1.293 +
   1.294 +\bibitem{plaisted90}
   1.295 +Plaisted, D.~A.,
   1.296 +\newblock A sequent-style model elimination strategy and a positive refinement,
   1.297 +\newblock {\em J. Auto. Reas. {\bf 6}}, 4 (1990), 389--402
   1.298 +
   1.299 +\bibitem{quaife92}
   1.300 +Quaife, A.,
   1.301 +\newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory,
   1.302 +\newblock {\em J. Auto. Reas. {\bf 8}}, 1 (1992), 91--147
   1.303 +
   1.304 +\bibitem{sawamura92}
   1.305 +Sawamura, H., Minami, T., Ohashi, K.,
   1.306 +\newblock Proof methods based on sheet of thought in {EUODHILOS},
   1.307 +\newblock Research Report IIAS-RR-92-6E, International Institute for Advanced
   1.308 +  Study of Social Information Science, Fujitsu Laboratories, 1992
   1.309 +
   1.310 +\bibitem{suppes72}
   1.311 +Suppes, P.,
   1.312 +\newblock {\em Axiomatic Set Theory},
   1.313 +\newblock Dover, 1972
   1.314 +
   1.315 +\bibitem{takeuti87}
   1.316 +Takeuti, G.,
   1.317 +\newblock {\em Proof Theory}, 2nd~ed.,
   1.318 +\newblock North Holland, 1987
   1.319 +
   1.320 +\bibitem{thompson91}
   1.321 +Thompson, S.,
   1.322 +\newblock {\em Type Theory and Functional Programming},
   1.323 +\newblock Addison-Wesley, 1991
   1.324 +
   1.325 +\bibitem{principia}
   1.326 +Whitehead, A.~N., Russell, B.,
   1.327 +\newblock {\em Principia Mathematica},
   1.328 +\newblock Cambridge Univ. Press, 1962,
   1.329 +\newblock Paperback edition to *56, abridged from the 2nd edition (1927)
   1.330 +
   1.331 +\bibitem{wos-bledsoe}
   1.332 +Wos, L.,
   1.333 +\newblock Automated reasoning and {Bledsoe's} dream for the field,
   1.334 +\newblock In {\em Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
   1.335 +  R.~S. Boyer, Ed. Kluwer Academic Publishers, 1991, pp.~297--342
   1.336 +
   1.337 +\end{thebibliography}