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}