6592

1 
% BibTeX database for the Isabelle documentation


2 
%


3 
% Lawrence C Paulson $Id$


4 


5 
%publishers


6 
@string{AP="Academic Press"}


7 
@string{CUP="Cambridge University Press"}


8 
@string{IEEE="{\sc ieee} Computer Society Press"}


9 
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}


10 
@string{MIT="MIT Press"}


11 
@string{NH="NorthHolland"}


12 
@string{Prentice="PrenticeHall"}


13 
@string{Springer="SpringerVerlag"}


14 


15 
%institutions


16 
@string{CUCL="Computer Laboratory, University of Cambridge"}


17 


18 
%journals


19 
@string{FAC="Formal Aspects Comput."}


20 
@string{JAR="J. Auto. Reas."}


21 
@string{JCS="J. Comput. Secur."}


22 
@string{JFP="J. Func. Prog."}


23 
@string{JLC="J. Logic and Comput."}


24 
@string{JLP="J. Logic Prog."}


25 
@string{JSC="J. Symb. Comput."}


26 
@string{JSL="J. Symb. Logic"}


27 
@string{SIGPLAN="{SIGPLAN} Notices"}


28 


29 
%conferences


30 
@string{CADE="International Conference on Automated Deduction"}


31 
@string{POPL="Symposium on Principles of Programming Languages"}


32 
@string{TYPES="Types for Proofs and Programs"}


33 


34 


35 
%A


36 


37 
@incollection{abramsky90,


38 
author = {Samson Abramsky},


39 
title = {The Lazy Lambda Calculus},


40 
pages = {65116},


41 
editor = {David A. Turner},


42 
booktitle = {Research Topics in Functional Programming},


43 
publisher = {AddisonWesley},


44 
year = 1990}


45 


46 
@Unpublished{abrial93,


47 
author = {J. R. Abrial and G. Laffitte},


48 
title = {Towards the Mechanization of the Proofs of some Classical


49 
Theorems of Set Theory},


50 
note = {preprint},


51 
year = 1993,


52 
month = Feb}


53 


54 
@incollection{aczel77,


55 
author = {Peter Aczel},


56 
title = {An Introduction to Inductive Definitions},


57 
pages = {739782},


58 
crossref = {barwisehandbk}}


59 


60 
@Book{aczel88,


61 
author = {Peter Aczel},


62 
title = {NonWellFounded Sets},


63 
publisher = {CSLI},


64 
year = 1988}


65 


66 
@InProceedings{alf,


67 
author = {Lena Magnusson and Bengt {Nordstr\"{o}m}},


68 
title = {The {ALF} Proof Editor and Its Proof Engine},


69 
crossref = {types93},


70 
pages = {213237}}


71 


72 
@book{andrews86,


73 
author = "Peter Andrews",


74 
title = "An Introduction to Mathematical Logic and Type Theory: to Truth


75 
through Proof",


76 
publisher = AP,


77 
series = "Computer Science and Applied Mathematics",


78 
year = 1986}


79 


80 
%B


81 


82 
@incollection{basin91,


83 
author = {David Basin and Matt Kaufmann},


84 
title = {The {BoyerMoore} Prover and {Nuprl}: An Experimental


85 
Comparison},


86 
crossref = {huetplotkin91},


87 
pages = {89119}}


88 


89 
@Article{boyer86,


90 
author = {Robert Boyer and Ewing Lusk and William McCune and Ross


91 
Overbeek and Mark Stickel and Lawrence Wos},


92 
title = {Set Theory in FirstOrder Logic: Clauses for {G\"{o}del's}


93 
Axioms},


94 
journal = JAR,


95 
year = 1986,


96 
volume = 2,


97 
number = 3,


98 
pages = {287327}}


99 


100 
@book{bm79,


101 
author = {Robert S. Boyer and J Strother Moore},


102 
title = {A Computational Logic},


103 
publisher = {Academic Press},


104 
year = 1979}


105 


106 
@book{bm88book,


107 
author = {Robert S. Boyer and J Strother Moore},


108 
title = {A Computational Logic Handbook},


109 
publisher = {Academic Press},


110 
year = 1988}


111 


112 
@Article{debruijn72,


113 
author = {N. G. de Bruijn},


114 
title = {Lambda Calculus Notation with Nameless Dummies,


115 
a Tool for Automatic Formula Manipulation,


116 
with Application to the {ChurchRosser Theorem}},


117 
journal = {Indag. Math.},


118 
volume = 34,


119 
pages = {381392},


120 
year = 1972}


121 


122 
%C


123 


124 
@TechReport{camilleri92,


125 
author = {J. Camilleri and T. F. Melham},


126 
title = {Reasoning with Inductively Defined Relations in the


127 
{HOL} Theorem Prover},


128 
institution = CUCL,


129 
year = 1992,


130 
number = 265,


131 
month = Aug}


132 


133 
@Book{charniak80,


134 
author = {E. Charniak and C. K. Riesbeck and D. V. McDermott},


135 
title = {Artificial Intelligence Programming},


136 
publisher = {Lawrence Erlbaum Associates},


137 
year = 1980}


138 


139 
@article{church40,


140 
author = "Alonzo Church",


141 
title = "A Formulation of the Simple Theory of Types",


142 
journal = JSL,


143 
year = 1940,


144 
volume = 5,


145 
pages = "5668"}


146 


147 
@PhdThesis{coen92,


148 
author = {Martin D. Coen},


149 
title = {Interactive Program Derivation},


150 
school = {University of Cambridge},


151 
note = {Computer Laboratory Technical Report 272},


152 
month = nov,


153 
year = 1992}


154 


155 
@book{constable86,


156 
author = {R. L. Constable and others},


157 
title = {Implementing Mathematics with the Nuprl Proof


158 
Development System},


159 
publisher = Prentice,


160 
year = 1986}


161 


162 
%D


163 


164 
@Book{davey&priestley,


165 
author = {B. A. Davey and H. A. Priestley},


166 
title = {Introduction to Lattices and Order},


167 
publisher = CUP,


168 
year = 1990}


169 


170 
@Book{devlin79,


171 
author = {Keith J. Devlin},


172 
title = {Fundamentals of Contemporary Set Theory},


173 
publisher = {Springer},


174 
year = 1979}


175 


176 
@book{dummett,


177 
author = {Michael Dummett},


178 
title = {Elements of Intuitionism},


179 
year = 1977,


180 
publisher = {Oxford University Press}}


181 


182 
@incollection{dybjer91,


183 
author = {Peter Dybjer},


184 
title = {Inductive Sets and Families in {MartinL\"of's} Type


185 
Theory and Their SetTheoretic Semantics},


186 
crossref = {huetplotkin91},


187 
pages = {280306}}


188 


189 
@Article{dyckhoff,


190 
author = {Roy Dyckhoff},


191 
title = {ContractionFree Sequent Calculi for Intuitionistic Logic},


192 
journal = JSL,


193 
year = 1992,


194 
volume = 57,


195 
number = 3,


196 
pages = {795807}}


197 


198 
%F


199 


200 
@InProceedings{felty91a,


201 
Author = {Amy Felty},


202 
Title = {A Logic Program for Transforming Sequent Proofs to Natural


203 
Deduction Proofs},


204 
crossref = {extensions91},


205 
pages = {157178}}


206 


207 
@TechReport{frost93,


208 
author = {Jacob Frost},


209 
title = {A Case Study of Coinduction in {Isabelle HOL}},


210 
institution = CUCL,


211 
number = 308,


212 
year = 1993,


213 
month = Aug}


214 


215 
%revised version of frost93


216 
@TechReport{frost95,


217 
author = {Jacob Frost},


218 
title = {A Case Study of Coinduction in {Isabelle}},


219 
institution = CUCL,


220 
number = 359,


221 
year = 1995,


222 
month = Feb}


223 


224 
@inproceedings{OBJ,


225 
author = {K. Futatsugi and J.A. Goguen and JeanPierre Jouannaud


226 
and J. Meseguer},


227 
title = {Principles of {OBJ2}},


228 
booktitle = POPL,


229 
year = 1985,


230 
pages = {5266}}


231 


232 
%G


233 


234 
@book{gallier86,


235 
author = {J. H. Gallier},


236 
title = {Logic for Computer Science:


237 
Foundations of Automatic Theorem Proving},


238 
year = 1986,


239 
publisher = {Harper \& Row}}


240 


241 
@Book{galton90,


242 
author = {Antony Galton},


243 
title = {Logic for Information Technology},


244 
publisher = {Wiley},


245 
year = 1990}


246 


247 
@InProceedings{gimenezcodifying,


248 
author = {Eduardo Gim{\'e}nez},


249 
title = {Codifying Guarded Definitions with Recursive Schemes},


250 
crossref = {types94},


251 
pages = {3959}


252 
}


253 


254 
@Book{mgordonhol,


255 
author = {M. J. C. Gordon and T. F. Melham},


256 
title = {Introduction to {HOL}: A Theorem Proving Environment for


257 
Higher Order Logic},


258 
publisher = CUP,


259 
year = 1993}


260 


261 
@book{mgordon79,


262 
author = {Michael J. C. Gordon and Robin Milner and Christopher P.


263 
Wadsworth},


264 
title = {Edinburgh {LCF}: A Mechanised Logic of Computation},


265 
year = 1979,


266 
publisher = {Springer},


267 
series = {LNCS 78}}


268 


269 
@InProceedings{guntertrees,


270 
author = {Elsa L. Gunter},


271 
title = {A Broader Class of Trees for Recursive Type Definitions for


272 
{HOL}},


273 
crossref = {hug93},


274 
pages = {141154}}


275 


276 
%H


277 


278 
@Book{halmos60,


279 
author = {Paul R. Halmos},


280 
title = {Naive Set Theory},


281 
publisher = {Van Nostrand},


282 
year = 1960}


283 


284 
@Book{hennessy90,


285 
author = {Matthew Hennessy},


286 
title = {The Semantics of Programming Languages: An Elementary


287 
Introduction Using Structural Operational Semantics},


288 
publisher = {Wiley},


289 
year = 1990}


290 


291 
@Article{haskellreport,


292 
author = {Paul Hudak and Simon Peyton Jones and Philip Wadler},


293 
title = {Report on the Programming Language {Haskell}: A


294 
Nonstrict, Purely Functional Language},


295 
journal = SIGPLAN,


296 
year = 1992,


297 
volume = 27,


298 
number = 5,


299 
month = May,


300 
note = {Version 1.2}}


301 


302 
@Article{haskelltutorial,


303 
author = {Paul Hudak and Joseph H. Fasel},


304 
title = {A Gentle Introduction to {Haskell}},


305 
journal = SIGPLAN,


306 
year = 1992,


307 
volume = 27,


308 
number = 5,


309 
month = May}


310 


311 
@article{huet75,


312 
author = {G. P. Huet},


313 
title = {A Unification Algorithm for Typed $\lambda$Calculus},


314 
journal = TCS,


315 
volume = 1,


316 
year = 1975,


317 
pages = {2757}}


318 


319 
@article{huet78,


320 
author = {G. P. Huet and B. Lang},


321 
title = {Proving and Applying Program Transformations Expressed with


322 
SecondOrder Patterns},


323 
journal = acta,


324 
volume = 11,


325 
year = 1978,


326 
pages = {3155}}


327 


328 
@inproceedings{huet88,


329 
author = {G\'erard Huet},


330 
title = {Induction Principles Formalized in the {Calculus of


331 
Constructions}},


332 
booktitle = {Programming of Future Generation Computers},


333 
editor = {K. Fuchi and M. Nivat},


334 
year = 1988,


335 
pages = {205216},


336 
publisher = {Elsevier}}


337 


338 
%K


339 


340 
@Book{kunen80,


341 
author = {Kenneth Kunen},


342 
title = {Set Theory: An Introduction to Independence Proofs},


343 
publisher = NH,


344 
year = 1980}


345 


346 
%M


347 


348 
@Article{mw81,


349 
author = {Zohar Manna and Richard Waldinger},


350 
title = {Deductive Synthesis of the Unification Algorithm},


351 
journal = SCP,


352 
year = 1981,


353 
volume = 1,


354 
number = 1,


355 
pages = {548}}


356 


357 
@InProceedings{martinnipkow,


358 
author = {Ursula Martin and Tobias Nipkow},


359 
title = {Ordered Rewriting and Confluence},


360 
crossref = {cade10},


361 
pages = {366380}}


362 


363 
@book{martinlof84,


364 
author = {Per MartinL\"of},


365 
title = {Intuitionistic type theory},


366 
year = 1984,


367 
publisher = {Bibliopolis}}


368 


369 
@incollection{melham89,


370 
author = {Thomas F. Melham},


371 
title = {Automating Recursive Type Definitions in Higher Order


372 
Logic},


373 
pages = {341386},


374 
crossref = {birtwistle89}}


375 


376 
@Article{millermixed,


377 
Author = {Dale Miller},


378 
Title = {Unification Under a Mixed Prefix},


379 
journal = JSC,


380 
volume = 14,


381 
number = 4,


382 
pages = {321358},


383 
Year = 1992}


384 


385 
@Article{milner78,


386 
author = {Robin Milner},


387 
title = {A Theory of Type Polymorphism in Programming},


388 
journal = "J. Comp.\ Sys.\ Sci.",


389 
year = 1978,


390 
volume = 17,


391 
pages = {348375}}


392 


393 
@TechReport{milnerind,


394 
author = {Robin Milner},


395 
title = {How to Derive Inductions in {LCF}},


396 
institution = Edinburgh,


397 
year = 1980,


398 
type = {note}}


399 


400 
@Article{milnercoind,


401 
author = {Robin Milner and Mads Tofte},


402 
title = {Coinduction in Relational Semantics},


403 
journal = TCS,


404 
year = 1991,


405 
volume = 87,


406 
pages = {209220}}


407 


408 
@Book{milner89,


409 
author = {Robin Milner},


410 
title = {Communication and Concurrency},


411 
publisher = Prentice,


412 
year = 1989}


413 


414 
@PhdThesis{monahan84,


415 
author = {Brian Q. Monahan},


416 
title = {Data Type Proofs using Edinburgh {LCF}},


417 
school = {University of Edinburgh},


418 
year = 1984}


419 


420 
%N


421 


422 
@InProceedings{NaraschewskiWTPHOLs98,


423 
author = {Wolfgang Naraschewski and Markus Wenzel},


424 
title =


425 
{ObjectOriented Verification based on Record Subtyping in HigherOrder Logic},


426 
booktitle = {Theorem Proving in Higher Order Logics (TPHOLs'98)},


427 
publisher = Springer,


428 
volume = 1479,


429 
series = LNCS,


430 
year = 1998}


431 


432 
@inproceedings{nazarethnipkow,


433 
author = {Dieter Nazareth and Tobias Nipkow},


434 
title = {Formal Verification of Algorithm {W}: The Monomorphic Case},


435 
crossref = {tphols96},


436 
pages = {331345},


437 
year = 1996}


438 


439 
@inproceedings{nipkowW,


440 
author = {Wolfgang Naraschewski and Tobias Nipkow},


441 
title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},


442 
booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96},


443 
editor = {E. Gim\'enez and C. PaulinMohring},


444 
publisher = Springer,


445 
series = LNCS,


446 
volume = 1512,


447 
pages = {317332},


448 
year = 1998}


449 


450 
@inproceedings{NipkowCR,


451 
author = {Tobias Nipkow},


452 
title = {More {ChurchRosser} Proofs (in {Isabelle/HOL})},


453 
booktitle = {Automated Deduction  CADE13},


454 
editor = {M. McRobbie and J.K. Slaney},


455 
publisher = Springer,


456 
series = LNCS,


457 
volume = 1104,


458 
pages = {733747},


459 
year = 1996}


460 


461 
% WAS NipkowLICS93


462 
@InProceedings{nipkowpatterns,


463 
title = {Functional Unification of HigherOrder Patterns},


464 
author = {Tobias Nipkow},


465 
pages = {6474},


466 
crossref = {lics8},


467 
url = {ftp://ftp.informatik.tumuenchen.de/local/lehrstuhl/nipkow/lics93.html},


468 
keywords = {unification}}


469 


470 
@article{nipkowIMP,


471 
author = {Tobias Nipkow},


472 
title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},


473 
journal = FAC,


474 
volume = 10,


475 
pages = {171186},


476 
year = 1998}


477 


478 
@article{nipkowprehofer,


479 
author = {Tobias Nipkow and Christian Prehofer},


480 
title = {Type Reconstruction for Type Classes},


481 
journal = JFP,


482 
volume = 5,


483 
number = 2,


484 
year = 1995,


485 
pages = {201224}}


486 


487 
@Article{noel,


488 
author = {Philippe No{\"e}l},


489 
title = {Experimenting with {Isabelle} in {ZF} Set Theory},


490 
journal = JAR,


491 
volume = 10,


492 
number = 1,


493 
pages = {1558},


494 
year = 1993}


495 


496 
@book{nordstrom90,


497 
author = {Bengt {Nordstr\"om} and Kent Petersson and Jan Smith},


498 
title = {Programming in {MartinL\"of}'s Type Theory. An


499 
Introduction},


500 
publisher = {Oxford University Press},


501 
year = 1990}


502 


503 
%O


504 


505 
@Manual{pvslanguage,


506 
title = {The {PVS} specification language},


507 
author = {S. Owre and N. Shankar and J. M. Rushby},


508 
organization = {Computer Science Laboratory, SRI International},


509 
address = {Menlo Park, CA},


510 
note = {Beta release},


511 
year = 1993,


512 
month = apr,


513 
url = {\verbhttp://www.csl.sri.com/reports/pvslanguage.dvi.Z}}


514 


515 
%P


516 


517 
% replaces paulin92


518 
@InProceedings{paulintlca,


519 
author = {Christine PaulinMohring},


520 
title = {Inductive Definitions in the System {Coq}: Rules and


521 
Properties},


522 
crossref = {tlca93},


523 
pages = {328345}}


524 


525 
@InProceedings{paulsonCADE,


526 
author = {Lawrence C. Paulson},


527 
title = {A Fixedpoint Approach to Implementing (Co)Inductive


528 
Definitions},


529 
pages = {148161},


530 
crossref = {cade12}}


531 


532 
@InProceedings{paulsonCOLOG,


533 
author = {Lawrence C. Paulson},


534 
title = {A Formulation of the Simple Theory of Types (for


535 
{Isabelle})},


536 
pages = {246274},


537 
crossref = {colog88},


538 
url = {http://www.cl.cam.ac.uk/Research/Reports/TR175lcpsimple.dvi.gz}}


539 


540 
@Article{paulsoncoind,


541 
author = {Lawrence C. Paulson},


542 
title = {Mechanizing Coinduction and Corecursion in HigherOrder


543 
Logic},


544 
journal = JLC,


545 
year = 1997,


546 
volume = 7,


547 
number = 2,


548 
month = mar,


549 
pages = {175204}}


550 


551 
@techreport{isabelleZF,


552 
author = {Lawrence C. Paulson},


553 
title = {{Isabelle}'s Logics: {FOL} and {ZF}},


554 
institution = CUCL,


555 
year = 1999}


556 


557 
@article{paulsonfound,


558 
author = {Lawrence C. Paulson},


559 
title = {The Foundation of a Generic Theorem Prover},


560 
journal = JAR,


561 
volume = 5,


562 
number = 3,


563 
pages = {363397},


564 
year = 1989,


565 
url = {http://www.cl.cam.ac.uk/Research/Reports/TR130lcpgenerictheoremprover.dvi.gz}}


566 


567 
%replaces paulsonfinal


568 
@Article{paulsonmscs,


569 
author = {Lawrence C. Paulson},


570 
title = {Final Coalgebras as Greatest Fixed Points in ZF Set Theory},


571 
journal = {Mathematical Structures in Computer Science},


572 
year = 1999,


573 
volume = 9,


574 
note = {in press}}


575 


576 
@InCollection{paulsongeneric,


577 
author = {Lawrence C. Paulson},


578 
title = {Generic Automatic Proof Tools},


579 
crossref = {wosfest},


580 
chapter = 3}


581 


582 
@Article{paulsongr,


583 
author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},


584 
title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of


585 
Choice},


586 
journal = JAR,


587 
year = 1996,


588 
volume = 17,


589 
number = 3,


590 
month = dec,


591 
pages = {291323}}


592 


593 
@InCollection{paulsonhandbook,


594 
author = {Lawrence C. Paulson},


595 
title = {Designing a Theorem Prover},


596 
crossref = {handbklics2},


597 
pages = {415475}}


598 


599 
@Book{paulsonisabook,


600 
author = {Lawrence C. Paulson},


601 
title = {Isabelle: A Generic Theorem Prover},


602 
publisher = {Springer},


603 
year = 1994,


604 
note = {LNCS 828}}


605 


606 
@InCollection{paulsonmarkt,


607 
author = {Lawrence C. Paulson},


608 
title = {Tool Support for Logics of Programs},


609 
booktitle = {Mathematical Methods in Program Development:


610 
Summer School Marktoberdorf 1996},


611 
publisher = {Springer},


612 
pages = {461498},


613 
year = {Published 1997},


614 
editor = {Manfred Broy},


615 
series = {NATO ASI Series F}}


616 


617 
%replaces PaulsonML and paulson91


618 
@book{paulsonml2,


619 
author = {Lawrence C. Paulson},


620 
title = {{ML} for the Working Programmer},


621 
year = 1996,


622 
edition = {2nd},


623 
publisher = CUP}


624 


625 
@article{paulsonnatural,


626 
author = {Lawrence C. Paulson},


627 
title = {Natural Deduction as Higherorder Resolution},


628 
journal = JLP,


629 
volume = 3,


630 
pages = {237258},


631 
year = 1986,


632 
url = {http://www.cl.cam.ac.uk/Research/Reports/TR82lcphigherorderresolution.dvi.gz}}


633 


634 
@Article{paulsonsetI,


635 
author = {Lawrence C. Paulson},


636 
title = {Set Theory for Verification: {I}. {From}


637 
Foundations to Functions},


638 
journal = JAR,


639 
volume = 11,


640 
number = 3,


641 
pages = {353389},


642 
year = 1993,


643 
url = {ftp://ftp.cl.cam.ac.uk/ml/setI.ps.gz}}


644 


645 
@Article{paulsonsetII,


646 
author = {Lawrence C. Paulson},


647 
title = {Set Theory for Verification: {II}. {Induction} and


648 
Recursion},


649 
journal = JAR,


650 
volume = 15,


651 
number = 2,


652 
pages = {167215},


653 
year = 1995,


654 
url = {http://www.cl.cam.ac.uk/Research/Reports/TR312lcpsetII.ps.gz}}


655 


656 
@article{paulson85,


657 
author = {Lawrence C. Paulson},


658 
title = {Verifying the Unification Algorithm in {LCF}},


659 
journal = SCP,


660 
volume = 5,


661 
pages = {143170},


662 
year = 1985}


663 


664 
%replqces PaulsonLCF


665 
@book{paulson87,


666 
author = {Lawrence C. Paulson},


667 
title = {Logic and Computation: Interactive proof with Cambridge


668 
LCF},


669 
year = 1987,


670 
publisher = CUP}


671 


672 
@incollection{paulson700,


673 
author = {Lawrence C. Paulson},


674 
title = {{Isabelle}: The Next 700 Theorem Provers},


675 
crossref = {odifreddi90},


676 
pages = {361386},


677 
url = {http://www.cl.cam.ac.uk/Research/Reports/TR143lcpexperience.dvi.gz}}


678 


679 
% replaces paulsonns and paulsonsecurity


680 
@Article{paulsonjcs,


681 
author = {Lawrence C. Paulson},


682 
title = {The Inductive Approach to Verifying Cryptographic Protocols},


683 
journal = JCS,


684 
year = 1998,


685 
volume = 6,


686 
pages = {85128}}


687 


688 
@article{pelletier86,


689 
author = {F. J. Pelletier},


690 
title = {Seventyfive Problems for Testing Automatic Theorem


691 
Provers},


692 
journal = JAR,


693 
volume = 2,


694 
pages = {191216},


695 
year = 1986,


696 
note = {Errata, JAR 4 (1988), 235236 and JAR 18 (1997), 135}}


697 


698 
@Article{pitts94,


699 
author = {Andrew M. Pitts},


700 
title = {A Coinduction Principle for Recursively Defined Domains},


701 
journal = TCS,


702 
volume = 124,


703 
pages = {195219},


704 
year = 1994}


705 


706 
@Article{plaisted90,


707 
author = {David A. Plaisted},


708 
title = {A SequentStyle Model Elimination Strategy and a Positive


709 
Refinement},


710 
journal = JAR,


711 
year = 1990,


712 
volume = 6,


713 
number = 4,


714 
pages = {389402}}


715 


716 
%Q


717 


718 
@Article{quaife92,


719 
author = {Art Quaife},


720 
title = {Automated Deduction in {von NeumannBernaysG\"{o}del} Set


721 
Theory},


722 
journal = JAR,


723 
year = 1992,


724 
volume = 8,


725 
number = 1,


726 
pages = {91147}}


727 


728 
%R


729 


730 
@TechReport{rasmussen95,


731 
author = {Ole Rasmussen},


732 
title = {The {ChurchRosser} Theorem in {Isabelle}: A Proof Porting


733 
Experiment},


734 
institution = {Computer Laboratory, University of Cambridge},


735 
year = 1995,


736 
number = 364,


737 
month = may,


738 
url = {http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364or200churchrosserisabelle.ps.gz}}


739 


740 
@Book{reeves90,


741 
author = {Steve Reeves and Michael Clarke},


742 
title = {Logic for Computer Science},


743 
publisher = {AddisonWesley},


744 
year = 1990}


745 


746 
%S


747 


748 
@inproceedings{saaltinkfme,


749 
author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and


750 
Dan Craigen and Irwin Meisels},


751 
title = {An {EVES} Data Abstraction Example},


752 
pages = {578596},


753 
crossref = {fme93}}


754 


755 
@inproceedings{slindtfl,


756 
author = {Konrad Slind},


757 
title = {Function Definition in Higher Order Logic},


758 
booktitle = {Theorem Proving in Higher Order Logics},


759 
editor = {J. von Wright and J. Grundy and J. Harrison},


760 
publisher = Springer,


761 
series = LNCS,


762 
volume = 1125,


763 
pages = {381397},


764 
year = 1996}


765 


766 
@book{suppes72,


767 
author = {Patrick Suppes},


768 
title = {Axiomatic Set Theory},


769 
year = 1972,


770 
publisher = {Dover}}


771 


772 
@InCollection{szasz93,


773 
author = {Nora Szasz},


774 
title = {A Machine Checked Proof that {Ackermann's} Function is not


775 
Primitive Recursive},


776 
crossref = {huetplotkin93},


777 
pages = {317338}}


778 


779 
%T


780 


781 
@book{takeuti87,


782 
author = {G. Takeuti},


783 
title = {Proof Theory},


784 
year = 1987,


785 
publisher = NH,


786 
edition = {2nd}}


787 


788 
@Book{thompson91,


789 
author = {Simon Thompson},


790 
title = {Type Theory and Functional Programming},


791 
publisher = {AddisonWesley},


792 
year = 1991}


793 


794 
%V


795 


796 
@Unpublished{voelker94,


797 
author = {Norbert V\"olker},


798 
title = {The Verification of a Timer Program using {Isabelle/HOL}},


799 
url = {ftp://ftp.fernunihagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz},


800 
year = 1994,


801 
month = aug}


802 


803 
%W


804 


805 
@book{principia,


806 
author = {A. N. Whitehead and B. Russell},


807 
title = {Principia Mathematica},


808 
year = 1962,


809 
publisher = CUP,


810 
note = {Paperback edition to *56,


811 
abridged from the 2nd edition (1927)}}


812 


813 
@book{winskel93,


814 
author = {Glynn Winskel},


815 
title = {The Formal Semantics of Programming Languages},


816 
publisher = MIT,year=1993}


817 


818 
@InCollection{wosbledsoe,


819 
author = {Larry Wos},


820 
title = {Automated Reasoning and {Bledsoe's} Dream for the Field},


821 
crossref = {bledsoefest},


822 
pages = {297342}}


823 


824 


825 
% CROSS REFERENCES


826 


827 
@book{handbklics2,


828 
editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},


829 
title = {Handbook of Logic in Computer Science},


830 
booktitle = {Handbook of Logic in Computer Science},


831 
publisher = {Oxford University Press},


832 
year = 1992,


833 
volume = 2}


834 


835 
@book{types93,


836 
editor = {Henk Barendregt and Tobias Nipkow},


837 
title = TYPES # {: International Workshop {TYPES '93}},


838 
booktitle = TYPES # {: International Workshop {TYPES '93}},


839 
year = {published 1994},


840 
publisher = {Springer},


841 
series = {LNCS 806}}


842 


843 
@Proceedings{tlca93,


844 
title = {Typed Lambda Calculi and Applications},


845 
booktitle = {Typed Lambda Calculi and Applications},


846 
editor = {M. Bezem and J.F. Groote},


847 
year = 1993,


848 
publisher = {Springer},


849 
series = {LNCS 664}}


850 


851 
@book{bledsoefest,


852 
title = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},


853 
booktitle = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},


854 
publisher = {Kluwer Academic Publishers},


855 
year = 1991,


856 
editor = {Robert S. Boyer}}


857 


858 
@Proceedings{cade12,


859 
editor = {Alan Bundy},


860 
title = {Automated Deduction  {CADE}12


861 
International Conference},


862 
booktitle = {Automated Deduction  {CADE}12


863 
International Conference},


864 
year = 1994,


865 
series = {LNAI 814},


866 
publisher = {Springer}}


867 


868 
@book{types94,


869 
editor = {Peter Dybjer and Bengt Nordstr{\"om} and Jan Smith},


870 
title = TYPES # {: International Workshop {TYPES '94}},


871 
booktitle = TYPES # {: International Workshop {TYPES '94}},


872 
year = 1995,


873 
publisher = {Springer},


874 
series = {LNCS 996}}


875 


876 
@book{huetplotkin91,


877 
editor = {{G\'erard} Huet and Gordon Plotkin},


878 
title = {Logical Frameworks},


879 
booktitle = {Logical Frameworks},


880 
publisher = CUP,


881 
year = 1991}


882 


883 
@proceedings{colog88,


884 
editor = {P. MartinL\"of and G. Mints},


885 
title = {COLOG88: International Conference on Computer Logic},


886 
booktitle = {COLOG88: International Conference on Computer Logic},


887 
year = {Published 1990},


888 
publisher = {Springer},


889 
organization = {Estonian Academy of Sciences},


890 
address = {Tallinn},


891 
series = {LNCS 417}}


892 


893 
@book{odifreddi90,


894 
editor = {P. Odifreddi},


895 
title = {Logic and Computer Science},


896 
booktitle = {Logic and Computer Science},


897 
publisher = {Academic Press},


898 
year = 1990}


899 


900 
@proceedings{extensions91,


901 
editor = {Peter SchroederHeister},


902 
title = {Extensions of Logic Programming},


903 
booktitle = {Extensions of Logic Programming},


904 
year = 1991,


905 
series = {LNAI 475},


906 
publisher = {Springer}}


907 


908 
@proceedings{cade10,


909 
editor = {Mark E. Stickel},


910 
title = {10th } # CADE,


911 
booktitle = {10th } # CADE,


912 
year = 1990,


913 
publisher = {Springer},


914 
series = {LNAI 449}}


915 


916 
@Proceedings{lics8,


917 
editor = {M. Vardi},


918 
title = {Eighth Annual Symposium on Logic in Computer Science},


919 
booktitle = {Eighth Annual Symposium on Logic in Computer Science},


920 
publisher = IEEE,


921 
year = 1993}


922 


923 
@book{wosfest,


924 
title = {Automated Reasoning and its Applications:


925 
Essays in Honor of {Larry Wos}},


926 
booktitle = {Automated Reasoning and its Applications:


927 
Essays in Honor of {Larry Wos}},


928 
publisher = {MIT Press},


929 
year = 1997,


930 
editor = {Robert Veroff}}


931 


932 
@Proceedings{tphols96,


933 
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},


934 
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},


935 
editor = {J. von Wright and J. Grundy and J. Harrison},


936 
series = {LNCS 1125},


937 
year = 1996}
