1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/manual.bib Wed May 05 16:44:42 1999 +0200
1.3 @@ -0,0 +1,937 @@
1.4 +% BibTeX database for the Isabelle documentation
1.5 +%
1.6 +% Lawrence C Paulson $Id$
1.7 +
1.8 +%publishers
1.9 +@string{AP="Academic Press"}
1.10 +@string{CUP="Cambridge University Press"}
1.11 +@string{IEEE="{\sc ieee} Computer Society Press"}
1.12 +@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
1.13 +@string{MIT="MIT Press"}
1.14 +@string{NH="North-Holland"}
1.15 +@string{Prentice="Prentice-Hall"}
1.16 +@string{Springer="Springer-Verlag"}
1.17 +
1.18 +%institutions
1.19 +@string{CUCL="Computer Laboratory, University of Cambridge"}
1.20 +
1.21 +%journals
1.22 +@string{FAC="Formal Aspects Comput."}
1.23 +@string{JAR="J. Auto. Reas."}
1.24 +@string{JCS="J. Comput. Secur."}
1.25 +@string{JFP="J. Func. Prog."}
1.26 +@string{JLC="J. Logic and Comput."}
1.27 +@string{JLP="J. Logic Prog."}
1.28 +@string{JSC="J. Symb. Comput."}
1.29 +@string{JSL="J. Symb. Logic"}
1.30 +@string{SIGPLAN="{SIGPLAN} Notices"}
1.31 +
1.32 +%conferences
1.33 +@string{CADE="International Conference on Automated Deduction"}
1.34 +@string{POPL="Symposium on Principles of Programming Languages"}
1.35 +@string{TYPES="Types for Proofs and Programs"}
1.36 +
1.37 +
1.38 +%A
1.39 +
1.40 +@incollection{abramsky90,
1.41 + author = {Samson Abramsky},
1.42 + title = {The Lazy Lambda Calculus},
1.43 + pages = {65-116},
1.44 + editor = {David A. Turner},
1.45 + booktitle = {Research Topics in Functional Programming},
1.46 + publisher = {Addison-Wesley},
1.47 + year = 1990}
1.48 +
1.49 +@Unpublished{abrial93,
1.50 + author = {J. R. Abrial and G. Laffitte},
1.51 + title = {Towards the Mechanization of the Proofs of some Classical
1.52 + Theorems of Set Theory},
1.53 + note = {preprint},
1.54 + year = 1993,
1.55 + month = Feb}
1.56 +
1.57 +@incollection{aczel77,
1.58 + author = {Peter Aczel},
1.59 + title = {An Introduction to Inductive Definitions},
1.60 + pages = {739-782},
1.61 + crossref = {barwise-handbk}}
1.62 +
1.63 +@Book{aczel88,
1.64 + author = {Peter Aczel},
1.65 + title = {Non-Well-Founded Sets},
1.66 + publisher = {CSLI},
1.67 + year = 1988}
1.68 +
1.69 +@InProceedings{alf,
1.70 + author = {Lena Magnusson and Bengt {Nordstr\"{o}m}},
1.71 + title = {The {ALF} Proof Editor and Its Proof Engine},
1.72 + crossref = {types93},
1.73 + pages = {213-237}}
1.74 +
1.75 +@book{andrews86,
1.76 + author = "Peter Andrews",
1.77 + title = "An Introduction to Mathematical Logic and Type Theory: to Truth
1.78 +through Proof",
1.79 + publisher = AP,
1.80 + series = "Computer Science and Applied Mathematics",
1.81 + year = 1986}
1.82 +
1.83 +%B
1.84 +
1.85 +@incollection{basin91,
1.86 + author = {David Basin and Matt Kaufmann},
1.87 + title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
1.88 + Comparison},
1.89 + crossref = {huet-plotkin91},
1.90 + pages = {89-119}}
1.91 +
1.92 +@Article{boyer86,
1.93 + author = {Robert Boyer and Ewing Lusk and William McCune and Ross
1.94 + Overbeek and Mark Stickel and Lawrence Wos},
1.95 + title = {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}
1.96 + Axioms},
1.97 + journal = JAR,
1.98 + year = 1986,
1.99 + volume = 2,
1.100 + number = 3,
1.101 + pages = {287-327}}
1.102 +
1.103 +@book{bm79,
1.104 + author = {Robert S. Boyer and J Strother Moore},
1.105 + title = {A Computational Logic},
1.106 + publisher = {Academic Press},
1.107 + year = 1979}
1.108 +
1.109 +@book{bm88book,
1.110 + author = {Robert S. Boyer and J Strother Moore},
1.111 + title = {A Computational Logic Handbook},
1.112 + publisher = {Academic Press},
1.113 + year = 1988}
1.114 +
1.115 +@Article{debruijn72,
1.116 + author = {N. G. de Bruijn},
1.117 + title = {Lambda Calculus Notation with Nameless Dummies,
1.118 + a Tool for Automatic Formula Manipulation,
1.119 + with Application to the {Church-Rosser Theorem}},
1.120 + journal = {Indag. Math.},
1.121 + volume = 34,
1.122 + pages = {381-392},
1.123 + year = 1972}
1.124 +
1.125 +%C
1.126 +
1.127 +@TechReport{camilleri92,
1.128 + author = {J. Camilleri and T. F. Melham},
1.129 + title = {Reasoning with Inductively Defined Relations in the
1.130 + {HOL} Theorem Prover},
1.131 + institution = CUCL,
1.132 + year = 1992,
1.133 + number = 265,
1.134 + month = Aug}
1.135 +
1.136 +@Book{charniak80,
1.137 + author = {E. Charniak and C. K. Riesbeck and D. V. McDermott},
1.138 + title = {Artificial Intelligence Programming},
1.139 + publisher = {Lawrence Erlbaum Associates},
1.140 + year = 1980}
1.141 +
1.142 +@article{church40,
1.143 + author = "Alonzo Church",
1.144 + title = "A Formulation of the Simple Theory of Types",
1.145 + journal = JSL,
1.146 + year = 1940,
1.147 + volume = 5,
1.148 + pages = "56-68"}
1.149 +
1.150 +@PhdThesis{coen92,
1.151 + author = {Martin D. Coen},
1.152 + title = {Interactive Program Derivation},
1.153 + school = {University of Cambridge},
1.154 + note = {Computer Laboratory Technical Report 272},
1.155 + month = nov,
1.156 + year = 1992}
1.157 +
1.158 +@book{constable86,
1.159 + author = {R. L. Constable and others},
1.160 + title = {Implementing Mathematics with the Nuprl Proof
1.161 + Development System},
1.162 + publisher = Prentice,
1.163 + year = 1986}
1.164 +
1.165 +%D
1.166 +
1.167 +@Book{davey&priestley,
1.168 + author = {B. A. Davey and H. A. Priestley},
1.169 + title = {Introduction to Lattices and Order},
1.170 + publisher = CUP,
1.171 + year = 1990}
1.172 +
1.173 +@Book{devlin79,
1.174 + author = {Keith J. Devlin},
1.175 + title = {Fundamentals of Contemporary Set Theory},
1.176 + publisher = {Springer},
1.177 + year = 1979}
1.178 +
1.179 +@book{dummett,
1.180 + author = {Michael Dummett},
1.181 + title = {Elements of Intuitionism},
1.182 + year = 1977,
1.183 + publisher = {Oxford University Press}}
1.184 +
1.185 +@incollection{dybjer91,
1.186 + author = {Peter Dybjer},
1.187 + title = {Inductive Sets and Families in {Martin-L\"of's} Type
1.188 + Theory and Their Set-Theoretic Semantics},
1.189 + crossref = {huet-plotkin91},
1.190 + pages = {280-306}}
1.191 +
1.192 +@Article{dyckhoff,
1.193 + author = {Roy Dyckhoff},
1.194 + title = {Contraction-Free Sequent Calculi for Intuitionistic Logic},
1.195 + journal = JSL,
1.196 + year = 1992,
1.197 + volume = 57,
1.198 + number = 3,
1.199 + pages = {795-807}}
1.200 +
1.201 +%F
1.202 +
1.203 +@InProceedings{felty91a,
1.204 + Author = {Amy Felty},
1.205 + Title = {A Logic Program for Transforming Sequent Proofs to Natural
1.206 + Deduction Proofs},
1.207 + crossref = {extensions91},
1.208 + pages = {157-178}}
1.209 +
1.210 +@TechReport{frost93,
1.211 + author = {Jacob Frost},
1.212 + title = {A Case Study of Co-induction in {Isabelle HOL}},
1.213 + institution = CUCL,
1.214 + number = 308,
1.215 + year = 1993,
1.216 + month = Aug}
1.217 +
1.218 +%revised version of frost93
1.219 +@TechReport{frost95,
1.220 + author = {Jacob Frost},
1.221 + title = {A Case Study of Co-induction in {Isabelle}},
1.222 + institution = CUCL,
1.223 + number = 359,
1.224 + year = 1995,
1.225 + month = Feb}
1.226 +
1.227 +@inproceedings{OBJ,
1.228 + author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
1.229 + and J. Meseguer},
1.230 + title = {Principles of {OBJ2}},
1.231 + booktitle = POPL,
1.232 + year = 1985,
1.233 + pages = {52-66}}
1.234 +
1.235 +%G
1.236 +
1.237 +@book{gallier86,
1.238 + author = {J. H. Gallier},
1.239 + title = {Logic for Computer Science:
1.240 + Foundations of Automatic Theorem Proving},
1.241 + year = 1986,
1.242 + publisher = {Harper \& Row}}
1.243 +
1.244 +@Book{galton90,
1.245 + author = {Antony Galton},
1.246 + title = {Logic for Information Technology},
1.247 + publisher = {Wiley},
1.248 + year = 1990}
1.249 +
1.250 +@InProceedings{gimenez-codifying,
1.251 + author = {Eduardo Gim{\'e}nez},
1.252 + title = {Codifying Guarded Definitions with Recursive Schemes},
1.253 + crossref = {types94},
1.254 + pages = {39-59}
1.255 +}
1.256 +
1.257 +@Book{mgordon-hol,
1.258 + author = {M. J. C. Gordon and T. F. Melham},
1.259 + title = {Introduction to {HOL}: A Theorem Proving Environment for
1.260 + Higher Order Logic},
1.261 + publisher = CUP,
1.262 + year = 1993}
1.263 +
1.264 +@book{mgordon79,
1.265 + author = {Michael J. C. Gordon and Robin Milner and Christopher P.
1.266 + Wadsworth},
1.267 + title = {Edinburgh {LCF}: A Mechanised Logic of Computation},
1.268 + year = 1979,
1.269 + publisher = {Springer},
1.270 + series = {LNCS 78}}
1.271 +
1.272 +@InProceedings{gunter-trees,
1.273 + author = {Elsa L. Gunter},
1.274 + title = {A Broader Class of Trees for Recursive Type Definitions for
1.275 + {HOL}},
1.276 + crossref = {hug93},
1.277 + pages = {141-154}}
1.278 +
1.279 +%H
1.280 +
1.281 +@Book{halmos60,
1.282 + author = {Paul R. Halmos},
1.283 + title = {Naive Set Theory},
1.284 + publisher = {Van Nostrand},
1.285 + year = 1960}
1.286 +
1.287 +@Book{hennessy90,
1.288 + author = {Matthew Hennessy},
1.289 + title = {The Semantics of Programming Languages: An Elementary
1.290 + Introduction Using Structural Operational Semantics},
1.291 + publisher = {Wiley},
1.292 + year = 1990}
1.293 +
1.294 +@Article{haskell-report,
1.295 + author = {Paul Hudak and Simon Peyton Jones and Philip Wadler},
1.296 + title = {Report on the Programming Language {Haskell}: A
1.297 + Non-strict, Purely Functional Language},
1.298 + journal = SIGPLAN,
1.299 + year = 1992,
1.300 + volume = 27,
1.301 + number = 5,
1.302 + month = May,
1.303 + note = {Version 1.2}}
1.304 +
1.305 +@Article{haskell-tutorial,
1.306 + author = {Paul Hudak and Joseph H. Fasel},
1.307 + title = {A Gentle Introduction to {Haskell}},
1.308 + journal = SIGPLAN,
1.309 + year = 1992,
1.310 + volume = 27,
1.311 + number = 5,
1.312 + month = May}
1.313 +
1.314 +@article{huet75,
1.315 + author = {G. P. Huet},
1.316 + title = {A Unification Algorithm for Typed $\lambda$-Calculus},
1.317 + journal = TCS,
1.318 + volume = 1,
1.319 + year = 1975,
1.320 + pages = {27-57}}
1.321 +
1.322 +@article{huet78,
1.323 + author = {G. P. Huet and B. Lang},
1.324 + title = {Proving and Applying Program Transformations Expressed with
1.325 + Second-Order Patterns},
1.326 + journal = acta,
1.327 + volume = 11,
1.328 + year = 1978,
1.329 + pages = {31-55}}
1.330 +
1.331 +@inproceedings{huet88,
1.332 + author = {G\'erard Huet},
1.333 + title = {Induction Principles Formalized in the {Calculus of
1.334 + Constructions}},
1.335 + booktitle = {Programming of Future Generation Computers},
1.336 + editor = {K. Fuchi and M. Nivat},
1.337 + year = 1988,
1.338 + pages = {205-216},
1.339 + publisher = {Elsevier}}
1.340 +
1.341 +%K
1.342 +
1.343 +@Book{kunen80,
1.344 + author = {Kenneth Kunen},
1.345 + title = {Set Theory: An Introduction to Independence Proofs},
1.346 + publisher = NH,
1.347 + year = 1980}
1.348 +
1.349 +%M
1.350 +
1.351 +@Article{mw81,
1.352 + author = {Zohar Manna and Richard Waldinger},
1.353 + title = {Deductive Synthesis of the Unification Algorithm},
1.354 + journal = SCP,
1.355 + year = 1981,
1.356 + volume = 1,
1.357 + number = 1,
1.358 + pages = {5-48}}
1.359 +
1.360 +@InProceedings{martin-nipkow,
1.361 + author = {Ursula Martin and Tobias Nipkow},
1.362 + title = {Ordered Rewriting and Confluence},
1.363 + crossref = {cade10},
1.364 + pages = {366-380}}
1.365 +
1.366 +@book{martinlof84,
1.367 + author = {Per Martin-L\"of},
1.368 + title = {Intuitionistic type theory},
1.369 + year = 1984,
1.370 + publisher = {Bibliopolis}}
1.371 +
1.372 +@incollection{melham89,
1.373 + author = {Thomas F. Melham},
1.374 + title = {Automating Recursive Type Definitions in Higher Order
1.375 + Logic},
1.376 + pages = {341-386},
1.377 + crossref = {birtwistle89}}
1.378 +
1.379 +@Article{miller-mixed,
1.380 + Author = {Dale Miller},
1.381 + Title = {Unification Under a Mixed Prefix},
1.382 + journal = JSC,
1.383 + volume = 14,
1.384 + number = 4,
1.385 + pages = {321-358},
1.386 + Year = 1992}
1.387 +
1.388 +@Article{milner78,
1.389 + author = {Robin Milner},
1.390 + title = {A Theory of Type Polymorphism in Programming},
1.391 + journal = "J. Comp.\ Sys.\ Sci.",
1.392 + year = 1978,
1.393 + volume = 17,
1.394 + pages = {348-375}}
1.395 +
1.396 +@TechReport{milner-ind,
1.397 + author = {Robin Milner},
1.398 + title = {How to Derive Inductions in {LCF}},
1.399 + institution = Edinburgh,
1.400 + year = 1980,
1.401 + type = {note}}
1.402 +
1.403 +@Article{milner-coind,
1.404 + author = {Robin Milner and Mads Tofte},
1.405 + title = {Co-induction in Relational Semantics},
1.406 + journal = TCS,
1.407 + year = 1991,
1.408 + volume = 87,
1.409 + pages = {209-220}}
1.410 +
1.411 +@Book{milner89,
1.412 + author = {Robin Milner},
1.413 + title = {Communication and Concurrency},
1.414 + publisher = Prentice,
1.415 + year = 1989}
1.416 +
1.417 +@PhdThesis{monahan84,
1.418 + author = {Brian Q. Monahan},
1.419 + title = {Data Type Proofs using Edinburgh {LCF}},
1.420 + school = {University of Edinburgh},
1.421 + year = 1984}
1.422 +
1.423 +%N
1.424 +
1.425 +@InProceedings{NaraschewskiW-TPHOLs98,
1.426 + author = {Wolfgang Naraschewski and Markus Wenzel},
1.427 + title =
1.428 +{Object-Oriented Verification based on Record Subtyping in Higher-Order Logic},
1.429 + booktitle = {Theorem Proving in Higher Order Logics (TPHOLs'98)},
1.430 + publisher = Springer,
1.431 + volume = 1479,
1.432 + series = LNCS,
1.433 + year = 1998}
1.434 +
1.435 +@inproceedings{nazareth-nipkow,
1.436 + author = {Dieter Nazareth and Tobias Nipkow},
1.437 + title = {Formal Verification of Algorithm {W}: The Monomorphic Case},
1.438 + crossref = {tphols96},
1.439 + pages = {331-345},
1.440 + year = 1996}
1.441 +
1.442 +@inproceedings{nipkow-W,
1.443 + author = {Wolfgang Naraschewski and Tobias Nipkow},
1.444 + title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
1.445 + booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96},
1.446 + editor = {E. Gim\'enez and C. Paulin-Mohring},
1.447 + publisher = Springer,
1.448 + series = LNCS,
1.449 + volume = 1512,
1.450 + pages = {317-332},
1.451 + year = 1998}
1.452 +
1.453 +@inproceedings{Nipkow-CR,
1.454 + author = {Tobias Nipkow},
1.455 + title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
1.456 + booktitle = {Automated Deduction --- CADE-13},
1.457 + editor = {M. McRobbie and J.K. Slaney},
1.458 + publisher = Springer,
1.459 + series = LNCS,
1.460 + volume = 1104,
1.461 + pages = {733-747},
1.462 + year = 1996}
1.463 +
1.464 +% WAS Nipkow-LICS-93
1.465 +@InProceedings{nipkow-patterns,
1.466 + title = {Functional Unification of Higher-Order Patterns},
1.467 + author = {Tobias Nipkow},
1.468 + pages = {64-74},
1.469 + crossref = {lics8},
1.470 + url = {ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html},
1.471 + keywords = {unification}}
1.472 +
1.473 +@article{nipkow-IMP,
1.474 + author = {Tobias Nipkow},
1.475 + title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
1.476 + journal = FAC,
1.477 + volume = 10,
1.478 + pages = {171-186},
1.479 + year = 1998}
1.480 +
1.481 +@article{nipkow-prehofer,
1.482 + author = {Tobias Nipkow and Christian Prehofer},
1.483 + title = {Type Reconstruction for Type Classes},
1.484 + journal = JFP,
1.485 + volume = 5,
1.486 + number = 2,
1.487 + year = 1995,
1.488 + pages = {201-224}}
1.489 +
1.490 +@Article{noel,
1.491 + author = {Philippe No{\"e}l},
1.492 + title = {Experimenting with {Isabelle} in {ZF} Set Theory},
1.493 + journal = JAR,
1.494 + volume = 10,
1.495 + number = 1,
1.496 + pages = {15-58},
1.497 + year = 1993}
1.498 +
1.499 +@book{nordstrom90,
1.500 + author = {Bengt {Nordstr\"om} and Kent Petersson and Jan Smith},
1.501 + title = {Programming in {Martin-L\"of}'s Type Theory. An
1.502 + Introduction},
1.503 + publisher = {Oxford University Press},
1.504 + year = 1990}
1.505 +
1.506 +%O
1.507 +
1.508 +@Manual{pvs-language,
1.509 + title = {The {PVS} specification language},
1.510 + author = {S. Owre and N. Shankar and J. M. Rushby},
1.511 + organization = {Computer Science Laboratory, SRI International},
1.512 + address = {Menlo Park, CA},
1.513 + note = {Beta release},
1.514 + year = 1993,
1.515 + month = apr,
1.516 + url = {\verb|http://www.csl.sri.com/reports/pvs-language.dvi.Z|}}
1.517 +
1.518 +%P
1.519 +
1.520 +% replaces paulin92
1.521 +@InProceedings{paulin-tlca,
1.522 + author = {Christine Paulin-Mohring},
1.523 + title = {Inductive Definitions in the System {Coq}: Rules and
1.524 + Properties},
1.525 + crossref = {tlca93},
1.526 + pages = {328-345}}
1.527 +
1.528 +@InProceedings{paulson-CADE,
1.529 + author = {Lawrence C. Paulson},
1.530 + title = {A Fixedpoint Approach to Implementing (Co)Inductive
1.531 + Definitions},
1.532 + pages = {148-161},
1.533 + crossref = {cade12}}
1.534 +
1.535 +@InProceedings{paulson-COLOG,
1.536 + author = {Lawrence C. Paulson},
1.537 + title = {A Formulation of the Simple Theory of Types (for
1.538 + {Isabelle})},
1.539 + pages = {246-274},
1.540 + crossref = {colog88},
1.541 + url = {http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}
1.542 +
1.543 +@Article{paulson-coind,
1.544 + author = {Lawrence C. Paulson},
1.545 + title = {Mechanizing Coinduction and Corecursion in Higher-Order
1.546 + Logic},
1.547 + journal = JLC,
1.548 + year = 1997,
1.549 + volume = 7,
1.550 + number = 2,
1.551 + month = mar,
1.552 + pages = {175-204}}
1.553 +
1.554 +@techreport{isabelle-ZF,
1.555 + author = {Lawrence C. Paulson},
1.556 + title = {{Isabelle}'s Logics: {FOL} and {ZF}},
1.557 + institution = CUCL,
1.558 + year = 1999}
1.559 +
1.560 +@article{paulson-found,
1.561 + author = {Lawrence C. Paulson},
1.562 + title = {The Foundation of a Generic Theorem Prover},
1.563 + journal = JAR,
1.564 + volume = 5,
1.565 + number = 3,
1.566 + pages = {363-397},
1.567 + year = 1989,
1.568 + url = {http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}
1.569 +
1.570 +%replaces paulson-final
1.571 +@Article{paulson-mscs,
1.572 + author = {Lawrence C. Paulson},
1.573 + title = {Final Coalgebras as Greatest Fixed Points in ZF Set Theory},
1.574 + journal = {Mathematical Structures in Computer Science},
1.575 + year = 1999,
1.576 + volume = 9,
1.577 + note = {in press}}
1.578 +
1.579 +@InCollection{paulson-generic,
1.580 + author = {Lawrence C. Paulson},
1.581 + title = {Generic Automatic Proof Tools},
1.582 + crossref = {wos-fest},
1.583 + chapter = 3}
1.584 +
1.585 +@Article{paulson-gr,
1.586 + author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
1.587 + title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of
1.588 + Choice},
1.589 + journal = JAR,
1.590 + year = 1996,
1.591 + volume = 17,
1.592 + number = 3,
1.593 + month = dec,
1.594 + pages = {291-323}}
1.595 +
1.596 +@InCollection{paulson-handbook,
1.597 + author = {Lawrence C. Paulson},
1.598 + title = {Designing a Theorem Prover},
1.599 + crossref = {handbk-lics2},
1.600 + pages = {415-475}}
1.601 +
1.602 +@Book{paulson-isa-book,
1.603 + author = {Lawrence C. Paulson},
1.604 + title = {Isabelle: A Generic Theorem Prover},
1.605 + publisher = {Springer},
1.606 + year = 1994,
1.607 + note = {LNCS 828}}
1.608 +
1.609 +@InCollection{paulson-markt,
1.610 + author = {Lawrence C. Paulson},
1.611 + title = {Tool Support for Logics of Programs},
1.612 + booktitle = {Mathematical Methods in Program Development:
1.613 + Summer School Marktoberdorf 1996},
1.614 + publisher = {Springer},
1.615 + pages = {461-498},
1.616 + year = {Published 1997},
1.617 + editor = {Manfred Broy},
1.618 + series = {NATO ASI Series F}}
1.619 +
1.620 +%replaces Paulson-ML and paulson91
1.621 +@book{paulson-ml2,
1.622 + author = {Lawrence C. Paulson},
1.623 + title = {{ML} for the Working Programmer},
1.624 + year = 1996,
1.625 + edition = {2nd},
1.626 + publisher = CUP}
1.627 +
1.628 +@article{paulson-natural,
1.629 + author = {Lawrence C. Paulson},
1.630 + title = {Natural Deduction as Higher-order Resolution},
1.631 + journal = JLP,
1.632 + volume = 3,
1.633 + pages = {237-258},
1.634 + year = 1986,
1.635 + url = {http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}
1.636 +
1.637 +@Article{paulson-set-I,
1.638 + author = {Lawrence C. Paulson},
1.639 + title = {Set Theory for Verification: {I}. {From}
1.640 + Foundations to Functions},
1.641 + journal = JAR,
1.642 + volume = 11,
1.643 + number = 3,
1.644 + pages = {353-389},
1.645 + year = 1993,
1.646 + url = {ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}
1.647 +
1.648 +@Article{paulson-set-II,
1.649 + author = {Lawrence C. Paulson},
1.650 + title = {Set Theory for Verification: {II}. {Induction} and
1.651 + Recursion},
1.652 + journal = JAR,
1.653 + volume = 15,
1.654 + number = 2,
1.655 + pages = {167-215},
1.656 + year = 1995,
1.657 + url = {http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}
1.658 +
1.659 +@article{paulson85,
1.660 + author = {Lawrence C. Paulson},
1.661 + title = {Verifying the Unification Algorithm in {LCF}},
1.662 + journal = SCP,
1.663 + volume = 5,
1.664 + pages = {143-170},
1.665 + year = 1985}
1.666 +
1.667 +%replqces Paulson-LCF
1.668 +@book{paulson87,
1.669 + author = {Lawrence C. Paulson},
1.670 + title = {Logic and Computation: Interactive proof with Cambridge
1.671 + LCF},
1.672 + year = 1987,
1.673 + publisher = CUP}
1.674 +
1.675 +@incollection{paulson700,
1.676 + author = {Lawrence C. Paulson},
1.677 + title = {{Isabelle}: The Next 700 Theorem Provers},
1.678 + crossref = {odifreddi90},
1.679 + pages = {361-386},
1.680 + url = {http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}
1.681 +
1.682 +% replaces paulson-ns and paulson-security
1.683 +@Article{paulson-jcs,
1.684 + author = {Lawrence C. Paulson},
1.685 + title = {The Inductive Approach to Verifying Cryptographic Protocols},
1.686 + journal = JCS,
1.687 + year = 1998,
1.688 + volume = 6,
1.689 + pages = {85-128}}
1.690 +
1.691 +@article{pelletier86,
1.692 + author = {F. J. Pelletier},
1.693 + title = {Seventy-five Problems for Testing Automatic Theorem
1.694 + Provers},
1.695 + journal = JAR,
1.696 + volume = 2,
1.697 + pages = {191-216},
1.698 + year = 1986,
1.699 + note = {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}
1.700 +
1.701 +@Article{pitts94,
1.702 + author = {Andrew M. Pitts},
1.703 + title = {A Co-induction Principle for Recursively Defined Domains},
1.704 + journal = TCS,
1.705 + volume = 124,
1.706 + pages = {195-219},
1.707 + year = 1994}
1.708 +
1.709 +@Article{plaisted90,
1.710 + author = {David A. Plaisted},
1.711 + title = {A Sequent-Style Model Elimination Strategy and a Positive
1.712 + Refinement},
1.713 + journal = JAR,
1.714 + year = 1990,
1.715 + volume = 6,
1.716 + number = 4,
1.717 + pages = {389-402}}
1.718 +
1.719 +%Q
1.720 +
1.721 +@Article{quaife92,
1.722 + author = {Art Quaife},
1.723 + title = {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set
1.724 + Theory},
1.725 + journal = JAR,
1.726 + year = 1992,
1.727 + volume = 8,
1.728 + number = 1,
1.729 + pages = {91-147}}
1.730 +
1.731 +%R
1.732 +
1.733 +@TechReport{rasmussen95,
1.734 + author = {Ole Rasmussen},
1.735 + title = {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
1.736 + Experiment},
1.737 + institution = {Computer Laboratory, University of Cambridge},
1.738 + year = 1995,
1.739 + number = 364,
1.740 + month = may,
1.741 + url = {http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}
1.742 +
1.743 +@Book{reeves90,
1.744 + author = {Steve Reeves and Michael Clarke},
1.745 + title = {Logic for Computer Science},
1.746 + publisher = {Addison-Wesley},
1.747 + year = 1990}
1.748 +
1.749 +%S
1.750 +
1.751 +@inproceedings{saaltink-fme,
1.752 + author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
1.753 + Dan Craigen and Irwin Meisels},
1.754 + title = {An {EVES} Data Abstraction Example},
1.755 + pages = {578-596},
1.756 + crossref = {fme93}}
1.757 +
1.758 +@inproceedings{slind-tfl,
1.759 + author = {Konrad Slind},
1.760 + title = {Function Definition in Higher Order Logic},
1.761 + booktitle = {Theorem Proving in Higher Order Logics},
1.762 + editor = {J. von Wright and J. Grundy and J. Harrison},
1.763 + publisher = Springer,
1.764 + series = LNCS,
1.765 + volume = 1125,
1.766 + pages = {381-397},
1.767 + year = 1996}
1.768 +
1.769 +@book{suppes72,
1.770 + author = {Patrick Suppes},
1.771 + title = {Axiomatic Set Theory},
1.772 + year = 1972,
1.773 + publisher = {Dover}}
1.774 +
1.775 +@InCollection{szasz93,
1.776 + author = {Nora Szasz},
1.777 + title = {A Machine Checked Proof that {Ackermann's} Function is not
1.778 + Primitive Recursive},
1.779 + crossref = {huet-plotkin93},
1.780 + pages = {317-338}}
1.781 +
1.782 +%T
1.783 +
1.784 +@book{takeuti87,
1.785 + author = {G. Takeuti},
1.786 + title = {Proof Theory},
1.787 + year = 1987,
1.788 + publisher = NH,
1.789 + edition = {2nd}}
1.790 +
1.791 +@Book{thompson91,
1.792 + author = {Simon Thompson},
1.793 + title = {Type Theory and Functional Programming},
1.794 + publisher = {Addison-Wesley},
1.795 + year = 1991}
1.796 +
1.797 +%V
1.798 +
1.799 +@Unpublished{voelker94,
1.800 + author = {Norbert V\"olker},
1.801 + title = {The Verification of a Timer Program using {Isabelle/HOL}},
1.802 + url = {ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz},
1.803 + year = 1994,
1.804 + month = aug}
1.805 +
1.806 +%W
1.807 +
1.808 +@book{principia,
1.809 + author = {A. N. Whitehead and B. Russell},
1.810 + title = {Principia Mathematica},
1.811 + year = 1962,
1.812 + publisher = CUP,
1.813 + note = {Paperback edition to *56,
1.814 + abridged from the 2nd edition (1927)}}
1.815 +
1.816 +@book{winskel93,
1.817 + author = {Glynn Winskel},
1.818 + title = {The Formal Semantics of Programming Languages},
1.819 + publisher = MIT,year=1993}
1.820 +
1.821 +@InCollection{wos-bledsoe,
1.822 + author = {Larry Wos},
1.823 + title = {Automated Reasoning and {Bledsoe's} Dream for the Field},
1.824 + crossref = {bledsoe-fest},
1.825 + pages = {297-342}}
1.826 +
1.827 +
1.828 +% CROSS REFERENCES
1.829 +
1.830 +@book{handbk-lics2,
1.831 + editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
1.832 + title = {Handbook of Logic in Computer Science},
1.833 + booktitle = {Handbook of Logic in Computer Science},
1.834 + publisher = {Oxford University Press},
1.835 + year = 1992,
1.836 + volume = 2}
1.837 +
1.838 +@book{types93,
1.839 + editor = {Henk Barendregt and Tobias Nipkow},
1.840 + title = TYPES # {: International Workshop {TYPES '93}},
1.841 + booktitle = TYPES # {: International Workshop {TYPES '93}},
1.842 + year = {published 1994},
1.843 + publisher = {Springer},
1.844 + series = {LNCS 806}}
1.845 +
1.846 +@Proceedings{tlca93,
1.847 + title = {Typed Lambda Calculi and Applications},
1.848 + booktitle = {Typed Lambda Calculi and Applications},
1.849 + editor = {M. Bezem and J.F. Groote},
1.850 + year = 1993,
1.851 + publisher = {Springer},
1.852 + series = {LNCS 664}}
1.853 +
1.854 +@book{bledsoe-fest,
1.855 + title = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
1.856 + booktitle = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
1.857 + publisher = {Kluwer Academic Publishers},
1.858 + year = 1991,
1.859 + editor = {Robert S. Boyer}}
1.860 +
1.861 +@Proceedings{cade12,
1.862 + editor = {Alan Bundy},
1.863 + title = {Automated Deduction --- {CADE}-12
1.864 + International Conference},
1.865 + booktitle = {Automated Deduction --- {CADE}-12
1.866 + International Conference},
1.867 + year = 1994,
1.868 + series = {LNAI 814},
1.869 + publisher = {Springer}}
1.870 +
1.871 +@book{types94,
1.872 + editor = {Peter Dybjer and Bengt Nordstr{\"om} and Jan Smith},
1.873 + title = TYPES # {: International Workshop {TYPES '94}},
1.874 + booktitle = TYPES # {: International Workshop {TYPES '94}},
1.875 + year = 1995,
1.876 + publisher = {Springer},
1.877 + series = {LNCS 996}}
1.878 +
1.879 +@book{huet-plotkin91,
1.880 + editor = {{G\'erard} Huet and Gordon Plotkin},
1.881 + title = {Logical Frameworks},
1.882 + booktitle = {Logical Frameworks},
1.883 + publisher = CUP,
1.884 + year = 1991}
1.885 +
1.886 +@proceedings{colog88,
1.887 + editor = {P. Martin-L\"of and G. Mints},
1.888 + title = {COLOG-88: International Conference on Computer Logic},
1.889 + booktitle = {COLOG-88: International Conference on Computer Logic},
1.890 + year = {Published 1990},
1.891 + publisher = {Springer},
1.892 + organization = {Estonian Academy of Sciences},
1.893 + address = {Tallinn},
1.894 + series = {LNCS 417}}
1.895 +
1.896 +@book{odifreddi90,
1.897 + editor = {P. Odifreddi},
1.898 + title = {Logic and Computer Science},
1.899 + booktitle = {Logic and Computer Science},
1.900 + publisher = {Academic Press},
1.901 + year = 1990}
1.902 +
1.903 +@proceedings{extensions91,
1.904 + editor = {Peter Schroeder-Heister},
1.905 + title = {Extensions of Logic Programming},
1.906 + booktitle = {Extensions of Logic Programming},
1.907 + year = 1991,
1.908 + series = {LNAI 475},
1.909 + publisher = {Springer}}
1.910 +
1.911 +@proceedings{cade10,
1.912 + editor = {Mark E. Stickel},
1.913 + title = {10th } # CADE,
1.914 + booktitle = {10th } # CADE,
1.915 + year = 1990,
1.916 + publisher = {Springer},
1.917 + series = {LNAI 449}}
1.918 +
1.919 +@Proceedings{lics8,
1.920 + editor = {M. Vardi},
1.921 + title = {Eighth Annual Symposium on Logic in Computer Science},
1.922 + booktitle = {Eighth Annual Symposium on Logic in Computer Science},
1.923 + publisher = IEEE,
1.924 + year = 1993}
1.925 +
1.926 +@book{wos-fest,
1.927 + title = {Automated Reasoning and its Applications:
1.928 + Essays in Honor of {Larry Wos}},
1.929 + booktitle = {Automated Reasoning and its Applications:
1.930 + Essays in Honor of {Larry Wos}},
1.931 + publisher = {MIT Press},
1.932 + year = 1997,
1.933 + editor = {Robert Veroff}}
1.934 +
1.935 +@Proceedings{tphols96,
1.936 + title = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
1.937 + booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
1.938 + editor = {J. von Wright and J. Grundy and J. Harrison},
1.939 + series = {LNCS 1125},
1.940 + year = 1996}