--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/manual.bib Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,2074 @@
+% BibTeX database for the Isabelle documentation
+
+%publishers
+@string{AP="Academic Press"}
+@string{CUP="Cambridge University Press"}
+@string{IEEE="IEEE Computer Society Press"}
+@string{LNCS="Lecture Notes in Computer Science"}
+@string{MIT="MIT Press"}
+@string{NH="North-Holland"}
+@string{Prentice="Prentice-Hall"}
+@string{PH="Prentice-Hall"}
+@string{Springer="Springer-Verlag"}
+
+%institutions
+@string{CUCL="Computer Laboratory, University of Cambridge"}
+@string{Edinburgh="Department of Computer Science, University of Edinburgh"}
+@string{TUM="Department of Informatics, Technical University of Munich"}
+
+%journals
+@string{AI="Artificial Intelligence"}
+@string{FAC="Formal Aspects of Computing"}
+@string{JAR="Journal of Automated Reasoning"}
+@string{JCS="Journal of Computer Security"}
+@string{JFP="Journal of Functional Programming"}
+@string{JLC="Journal of Logic and Computation"}
+@string{JLP="Journal of Logic Programming"}
+@string{JSC="Journal of Symbolic Computation"}
+@string{JSL="Journal of Symbolic Logic"}
+@string{PROYAL="Proceedings of the Royal Society of London"}
+@string{SIGPLAN="{SIGPLAN} Notices"}
+@string{TISSEC="ACM Transactions on Information and System Security"}
+
+%conferences
+@string{CADE="International Conference on Automated Deduction"}
+@string{POPL="Symposium on Principles of Programming Languages"}
+@string{TYPES="Types for Proofs and Programs"}
+
+
+%A
+
+@incollection{abramsky90,
+ author = {Samson Abramsky},
+ title = {The Lazy Lambda Calculus},
+ pages = {65-116},
+ editor = {David A. Turner},
+ booktitle = {Research Topics in Functional Programming},
+ publisher = {Addison-Wesley},
+ year = 1990}
+
+@Unpublished{abrial93,
+ author = {J. R. Abrial and G. Laffitte},
+ title = {Towards the Mechanization of the Proofs of Some Classical
+ Theorems of Set Theory},
+ note = {preprint},
+ year = 1993,
+ month = Feb}
+
+@incollection{aczel77,
+ author = {Peter Aczel},
+ title = {An Introduction to Inductive Definitions},
+ pages = {739-782},
+ crossref = {barwise-handbk}}
+
+@Book{aczel88,
+ author = {Peter Aczel},
+ title = {Non-Well-Founded Sets},
+ publisher = {CSLI},
+ year = 1988}
+
+@inproceedings{Aehlig-Haftmann-Nipkow:2008:nbe,
+ author = {Klaus Aehlig and Florian Haftmann and Tobias Nipkow},
+ title = {A Compiled Implementation of Normalization by Evaluation},
+ booktitle = {TPHOLs '08: Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics},
+ year = {2008},
+ isbn = {978-3-540-71065-3},
+ pages = {352--367},
+ publisher = Springer,
+ series = LNCS,
+ volume = {5170},
+ editor = {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar}
+}
+
+@InProceedings{alf,
+ author = {Lena Magnusson and Bengt {Nordstr\"{o}m}},
+ title = {The {ALF} Proof Editor and Its Proof Engine},
+ crossref = {types93},
+ pages = {213-237}}
+
+@inproceedings{andersson-1993,
+ author = "Arne Andersson",
+ title = "Balanced Search Trees Made Simple",
+ editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides",
+ booktitle = "WADS 1993",
+ series = LNCS,
+ volume = {709},
+ pages = "61--70",
+ year = 1993,
+ publisher = Springer}
+
+@book{andrews86,
+ author = "Peter Andrews",
+ title = "An Introduction to Mathematical Logic and Type Theory: to Truth
+through Proof",
+ publisher = AP,
+ series = "Computer Science and Applied Mathematics",
+ year = 1986}
+
+@InProceedings{Aspinall:2000:eProof,
+ author = {David Aspinall},
+ title = {Protocols for Interactive {e-Proof}},
+ booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)},
+ year = 2000,
+ note = {Unpublished work-in-progress paper,
+ \url{http://homepages.inf.ed.ac.uk/da/papers/drafts/eproof.ps.gz}}
+}
+
+@InProceedings{Aspinall:TACAS:2000,
+ author = {David Aspinall},
+ title = {{P}roof {G}eneral: A Generic Tool for Proof Development},
+ booktitle = {Tools and Algorithms for the Construction and Analysis of
+ Systems (TACAS)},
+ year = 2000,
+ publisher = Springer,
+ series = LNCS,
+ volume = 1785,
+ pages = "38--42"
+}
+
+@Misc{isamode,
+ author = {David Aspinall},
+ title = {Isamode --- {U}sing {I}sabelle with {E}macs},
+ note = {\url{http://homepages.inf.ed.ac.uk/da/Isamode/}}
+}
+
+@Misc{proofgeneral,
+ author = {David Aspinall},
+ title = {{P}roof {G}eneral},
+ note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+}
+
+%B
+
+@inproceedings{backes-brown-2010,
+ title = "Analytic Tableaux for Higher-Order Logic with Choice",
+ author = "Julian Backes and Chad E. Brown",
+ booktitle={Automated Reasoning: IJCAR 2010},
+ editor={J. Giesl and R. H\"ahnle},
+ publisher = Springer,
+ series = LNCS,
+ volume = 6173,
+ pages = "76--90",
+ year = 2010}
+
+@book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow},
+title="Term Rewriting and All That",publisher=CUP,year=1998}
+
+@manual{isabelle-locale,
+ author = {Clemens Ballarin},
+ title = {Tutorial to Locales and Locale Interpretation},
+ institution = TUM,
+ note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}}
+}
+
+@InCollection{Barendregt-Geuvers:2001,
+ author = {H. Barendregt and H. Geuvers},
+ title = {Proof Assistants using Dependent Type Systems},
+ booktitle = {Handbook of Automated Reasoning},
+ publisher = {Elsevier},
+ year = 2001,
+ editor = {A. Robinson and A. Voronkov}
+}
+
+@inproceedings{cvc3,
+ author = {Clark Barrett and Cesare Tinelli},
+ title = {{CVC3}},
+ booktitle = {CAV},
+ editor = {Werner Damm and Holger Hermanns},
+ volume = {4590},
+ series = LNCS,
+ pages = {298--302},
+ publisher = {Springer},
+ year = {2007}
+}
+
+@incollection{basin91,
+ author = {David Basin and Matt Kaufmann},
+ title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
+ Comparison},
+ crossref = {huet-plotkin91},
+ pages = {89-119}}
+
+@Unpublished{HOL-Library,
+ author = {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and
+ Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and
+ Markus Wenzel},
+ title = {The Supplemental {Isabelle/HOL} Library},
+ note = {Part of the Isabelle distribution,
+ \url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
+ year = 2002
+}
+
+@InProceedings{Bauer-Wenzel:2000:HB,
+ author = {Gertrud Bauer and Markus Wenzel},
+ title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
+ {I}sabelle/{I}sar},
+ booktitle = {Types for Proofs and Programs: TYPES'99},
+ editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
+ and Jan Smith},
+ series = {LNCS},
+ year = 2000
+}
+
+@InProceedings{Bauer-Wenzel:2001,
+ author = {Gertrud Bauer and Markus Wenzel},
+ title = {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
+ crossref = {tphols2001}}
+
+@inproceedings{leo2,
+ author = "Christoph Benzm{\"u}ller and Lawrence C. Paulson and Frank Theiss and Arnaud Fietzke",
+ title = "{LEO-II}---A Cooperative Automatic Theorem Prover for Higher-Order Logic",
+ editor = "Alessandro Armando and Peter Baumgartner and Gilles Dowek",
+ booktitle = "Automated Reasoning: IJCAR 2008",
+ publisher = Springer,
+ series = LNCS,
+ volume = 5195,
+ pages = "162--170",
+ year = 2008}
+
+@inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL,
+ author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
+ booktitle = {Theorem Proving in Higher Order Logics},
+ pages = {131--146},
+ title = {Turning Inductive into Equational Specifications},
+ year = {2009}
+}
+
+@INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
+ crossref = "tphols2000",
+ title = "Proof terms for simply typed higher order logic",
+ author = "Stefan Berghofer and Tobias Nipkow",
+ pages = "38--52"}
+
+@inproceedings{berghofer-nipkow-2004,
+ author = {Stefan Berghofer and Tobias Nipkow},
+ title = {Random Testing in {I}sabelle/{HOL}},
+ pages = {230--239},
+ editor = "J. Cuellar and Z. Liu",
+ booktitle = {{SEFM} 2004},
+ publisher = IEEE,
+ year = 2004}
+
+@InProceedings{Berghofer-Nipkow:2002,
+ author = {Stefan Berghofer and Tobias Nipkow},
+ title = {Executing Higher Order Logic},
+ booktitle = {Types for Proofs and Programs: TYPES'2000},
+ editor = {P. Callaghan and Z. Luo and J. McKinna and R. Pollack},
+ series = LNCS,
+ publisher = Springer,
+ volume = 2277,
+ year = 2002}
+
+@InProceedings{Berghofer-Wenzel:1999:TPHOL,
+ author = {Stefan Berghofer and Markus Wenzel},
+ title = {Inductive datatypes in {HOL} --- lessons learned in
+ {F}ormal-{L}ogic {E}ngineering},
+ crossref = {tphols99}}
+
+
+@InProceedings{Bezem-Coquand:2005,
+ author = {M.A. Bezem and T. Coquand},
+ title = {Automating {Coherent Logic}},
+ booktitle = {LPAR-12},
+ editor = {G. Sutcliffe and A. Voronkov},
+ volume = 3835,
+ series = LNCS,
+ publisher = Springer}
+
+@book{Bird-Wadler,author="Richard Bird and Philip Wadler",
+title="Introduction to Functional Programming",publisher=PH,year=1988}
+
+@book{Bird-Haskell,author="Richard Bird",
+title="Introduction to Functional Programming using Haskell",
+publisher=PH,year=1998}
+
+@manual{isabelle-nitpick,
+ author = {Jasmin Christian Blanchette},
+ title = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle/{HOL}},
+ institution = TUM,
+ note = {\url{http://isabelle.in.tum.de/doc/nitpick.pdf}}
+}
+
+@manual{isabelle-sledgehammer,
+ author = {Jasmin Christian Blanchette},
+ title = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle/{HOL}},
+ institution = TUM,
+ note = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}
+}
+
+@inproceedings{blanchette-nipkow-2010,
+ title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
+ author = "Jasmin Christian Blanchette and Tobias Nipkow",
+ crossref = {itp2010}}
+
+@inproceedings{why3,
+ author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
+ title = {{Why3}: Shepherd Your Herd of Provers},
+ editor = "K. Rustan M. Leino and Micha\l{} Moskal",
+ booktitle = {Boogie 2011},
+ pages = "53--64",
+ year = 2011
+}
+
+@inproceedings{alt-ergo,
+ author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean and St\'ephane Lescuyer},
+ title = {Implementing Polymorphism in {SMT} Solvers},
+ booktitle = {SMT '08},
+ pages = "1--5",
+ publisher = "ACM",
+ series = "ICPS",
+ year = 2008,
+ editor = {Clark Barrett and Leonardo de Moura}}
+% /BPR
+% and Domagoj Babic and Amit Goel
+
+@inproceedings{boehme-nipkow-2010,
+ author={Sascha B\"ohme and Tobias Nipkow},
+ title={Sledgehammer: Judgement Day},
+ booktitle={Automated Reasoning: IJCAR 2010},
+ editor={J. Giesl and R. H\"ahnle},
+ publisher=Springer,
+ series=LNCS,
+ volume = 6173,
+ pages = "107--121",
+ year=2010}
+
+@Article{boyer86,
+ author = {Robert Boyer and Ewing Lusk and William McCune and Ross
+ Overbeek and Mark Stickel and Lawrence Wos},
+ title = {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}
+ Axioms},
+ journal = JAR,
+ year = 1986,
+ volume = 2,
+ number = 3,
+ pages = {287-327}}
+
+@book{bm79,
+ author = {Robert S. Boyer and J Strother Moore},
+ title = {A Computational Logic},
+ publisher = {Academic Press},
+ year = 1979}
+
+@book{bm88book,
+ author = {Robert S. Boyer and J Strother Moore},
+ title = {A Computational Logic Handbook},
+ publisher = {Academic Press},
+ year = 1988}
+
+@inproceedings{satallax,
+ author = "Chad E. Brown",
+ title = "Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems",
+ booktitle = {Automated Deduction --- CADE-23},
+ publisher = Springer,
+ series = LNCS,
+ volume = 6803,
+ pages = "147--161",
+ editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
+ year = 2011}
+
+@Article{debruijn72,
+ author = {N. G. de Bruijn},
+ title = {Lambda Calculus Notation with Nameless Dummies,
+ a Tool for Automatic Formula Manipulation,
+ with Application to the {Church-Rosser Theorem}},
+ journal = {Indag. Math.},
+ volume = 34,
+ pages = {381-392},
+ year = 1972}
+
+@InProceedings{bulwahnKN07,
+ author = {Lukas Bulwahn and Alexander Krauss and Tobias Nipkow},
+ title = {Finding Lexicographic Orders for Termination Proofs in {Isabelle/HOL}},
+ crossref = {tphols2007},
+ pages = {38--53}
+}
+
+@InProceedings{bulwahn-et-al:2008:imperative,
+ author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
+ title = {Imperative Functional Programming with {Isabelle/HOL}},
+ crossref = {tphols2008},
+}
+% pages = {38--53}
+
+@Article{ban89,
+ author = {M. Burrows and M. Abadi and R. M. Needham},
+ title = {A Logic of Authentication},
+ journal = PROYAL,
+ year = 1989,
+ volume = 426,
+ pages = {233-271}}
+
+%C
+
+@InProceedings{Chaieb-Wenzel:2007,
+ author = {Amine Chaieb and Makarius Wenzel},
+ title = {Context aware Calculation and Deduction ---
+ Ring Equalities via {Gr\"obner Bases} in {Isabelle}},
+ booktitle = {Towards Mechanized Mathematical Assistants (CALCULEMUS 2007)},
+ editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
+ series = LNAI,
+ volume = 4573,
+ year = 2007,
+ publisher = Springer
+}
+
+@TechReport{camilleri92,
+ author = {J. Camilleri and T. F. Melham},
+ title = {Reasoning with Inductively Defined Relations in the
+ {HOL} Theorem Prover},
+ institution = CUCL,
+ year = 1992,
+ number = 265,
+ month = Aug}
+
+@Book{charniak80,
+ author = {E. Charniak and C. K. Riesbeck and D. V. McDermott},
+ title = {Artificial Intelligence Programming},
+ publisher = {Lawrence Erlbaum Associates},
+ year = 1980}
+
+@article{church40,
+ author = "Alonzo Church",
+ title = "A Formulation of the Simple Theory of Types",
+ journal = JSL,
+ year = 1940,
+ volume = 5,
+ pages = "56-68"}
+
+@book{ClarkeGP-book,author="Edmund Clarke and Orna Grumberg and Doron Peled",
+title="Model Checking",publisher=MIT,year=1999}
+
+@PhdThesis{coen92,
+ author = {Martin D. Coen},
+ title = {Interactive Program Derivation},
+ school = {University of Cambridge},
+ note = {Computer Laboratory Technical Report 272},
+ month = nov,
+ year = 1992}
+
+@book{constable86,
+ author = {R. L. Constable and others},
+ title = {Implementing Mathematics with the Nuprl Proof
+ Development System},
+ publisher = Prentice,
+ year = 1986}
+
+%D
+
+@Book{davey-priestley,
+ author = {B. A. Davey and H. A. Priestley},
+ title = {Introduction to Lattices and Order},
+ publisher = CUP,
+ year = 1990}
+
+@Book{devlin79,
+ author = {Keith J. Devlin},
+ title = {Fundamentals of Contemporary Set Theory},
+ publisher = {Springer},
+ year = 1979}
+
+@book{dummett,
+ author = {Michael Dummett},
+ title = {Elements of Intuitionism},
+ year = 1977,
+ publisher = {Oxford University Press}}
+
+@misc{yices,
+ author = {Bruno Dutertre and Leonardo de Moura},
+ title = {The {Yices} {SMT} Solver},
+ howpublished = "\url{http://yices.csl.sri.com/tool-paper.pdf}",
+ year = 2006}
+
+@incollection{dybjer91,
+ author = {Peter Dybjer},
+ title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type
+ Theory and Their Set-Theoretic Semantics},
+ crossref = {huet-plotkin91},
+ pages = {280-306}}
+
+@Article{dyckhoff,
+ author = {Roy Dyckhoff},
+ title = {Contraction-Free Sequent Calculi for Intuitionistic Logic},
+ journal = JSL,
+ year = 1992,
+ volume = 57,
+ number = 3,
+ pages = {795-807}}
+
+%F
+
+@Article{IMPS,
+ author = {William M. Farmer and Joshua D. Guttman and F. Javier
+ Thayer},
+ title = {{IMPS}: An Interactive Mathematical Proof System},
+ journal = JAR,
+ volume = 11,
+ number = 2,
+ year = 1993,
+ pages = {213-248}}
+
+@InProceedings{felty91a,
+ Author = {Amy Felty},
+ Title = {A Logic Program for Transforming Sequent Proofs to Natural
+ Deduction Proofs},
+ crossref = {extensions91},
+ pages = {157-178}}
+
+@Article{fleuriot-jcm,
+ author = {Jacques Fleuriot and Lawrence C. Paulson},
+ title = {Mechanizing Nonstandard Real Analysis},
+ journal = {LMS Journal of Computation and Mathematics},
+ year = 2000,
+ volume = 3,
+ pages = {140-190},
+ note = {\url{http://www.lms.ac.uk/jcm/3/lms1999-027/}}
+}
+
+@TechReport{frost93,
+ author = {Jacob Frost},
+ title = {A Case Study of Co-induction in {Isabelle HOL}},
+ institution = CUCL,
+ number = 308,
+ year = 1993,
+ month = Aug}
+
+%revised version of frost93
+@TechReport{frost95,
+ author = {Jacob Frost},
+ title = {A Case Study of Co-induction in {Isabelle}},
+ institution = CUCL,
+ number = 359,
+ year = 1995,
+ month = Feb}
+
+@inproceedings{OBJ,
+ author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
+ and J. Meseguer},
+ title = {Principles of {OBJ2}},
+ booktitle = POPL,
+ year = 1985,
+ pages = {52-66}}
+
+%G
+
+@book{gallier86,
+ author = {J. H. Gallier},
+ title = {Logic for Computer Science:
+ Foundations of Automatic Theorem Proving},
+ year = 1986,
+ publisher = {Harper \& Row}}
+
+@Book{galton90,
+ author = {Antony Galton},
+ title = {Logic for Information Technology},
+ publisher = {Wiley},
+ year = 1990}
+
+@Article{Gentzen:1935,
+ author = {G. Gentzen},
+ title = {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en},
+ journal = {Math. Zeitschrift},
+ year = 1935
+}
+
+@InProceedings{gimenez-codifying,
+ author = {Eduardo Gim{\'e}nez},
+ title = {Codifying Guarded Definitions with Recursive Schemes},
+ crossref = {types94},
+ pages = {39-59}
+}
+
+@book{girard89,
+ author = {Jean-Yves Girard},
+ title = {Proofs and Types},
+ year = 1989,
+ publisher = CUP,
+ note = {Translated by Yves LaFont and Paul Taylor}}
+
+@Book{mgordon-hol,
+ editor = {M. J. C. Gordon and T. F. Melham},
+ title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
+ publisher = CUP,
+ year = 1993}
+
+@book{mgordon79,
+ author = {Michael J. C. Gordon and Robin Milner and Christopher P.
+ Wadsworth},
+ title = {Edinburgh {LCF}: A Mechanised Logic of Computation},
+ year = 1979,
+ publisher = {Springer},
+ series = {LNCS 78}}
+
+@inproceedings{Gunter-HOL92,author={Elsa L. Gunter},
+title={Why we can't have {SML} style datatype declarations in {HOL}},
+booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\
+IFIP TC10/WG10.2 Intl. Workshop, 1992},
+editor={L.J.M. Claesen and M.J.C. Gordon},
+publisher=NH,year=1993,pages={561--568}}
+
+@InProceedings{gunter-trees,
+ author = {Elsa L. Gunter},
+ title = {A Broader Class of Trees for Recursive Type Definitions for
+ {HOL}},
+ crossref = {hug93},
+ pages = {141-154}}
+
+%H
+
+@InProceedings{Haftmann-Wenzel:2006:classes,
+ author = {Florian Haftmann and Makarius Wenzel},
+ title = {Constructive Type Classes in {Isabelle}},
+ editor = {T. Altenkirch and C. McBride},
+ booktitle = {Types for Proofs and Programs, TYPES 2006},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4502},
+ year = {2007}
+}
+
+@inproceedings{Haftmann-Nipkow:2010:code,
+ author = {Florian Haftmann and Tobias Nipkow},
+ title = {Code Generation via Higher-Order Rewrite Systems},
+ booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010},
+ year = 2010,
+ publisher = Springer,
+ series = LNCS,
+ editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
+ volume = 6009
+}
+
+@InProceedings{Haftmann-Wenzel:2009,
+ author = {Florian Haftmann and Makarius Wenzel},
+ title = {Local theory specifications in {Isabelle/Isar}},
+ editor = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo},
+ booktitle = {Types for Proofs and Programs, TYPES 2008},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {5497},
+ year = {2009}
+}
+
+@inproceedings{hindleymilner,
+ author = {L. Damas and H. Milner},
+ title = {Principal type schemes for functional programs},
+ booktitle = {ACM Symp. Principles of Programming Languages},
+ year = 1982
+}
+
+@manual{isabelle-classes,
+ author = {Florian Haftmann},
+ title = {Haskell-style type classes with {Isabelle}/{Isar}},
+ institution = TUM,
+ note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}
+}
+
+@manual{isabelle-codegen,
+ author = {Florian Haftmann},
+ title = {Code generation from Isabelle theories},
+ institution = TUM,
+ note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}
+}
+
+@Book{halmos60,
+ author = {Paul R. Halmos},
+ title = {Naive Set Theory},
+ publisher = {Van Nostrand},
+ year = 1960}
+
+@book{HarelKT-DL,author={David Harel and Dexter Kozen and Jerzy Tiuryn},
+title={Dynamic Logic},publisher=MIT,year=2000}
+
+@Book{hennessy90,
+ author = {Matthew Hennessy},
+ title = {The Semantics of Programming Languages: An Elementary
+ Introduction Using Structural Operational Semantics},
+ publisher = {Wiley},
+ year = 1990}
+
+@article{waldmeister,
+ author = {Thomas Hillenbrand and Arnim Buch and Rolan Vogt and Bernd L\"ochner},
+ title = "Waldmeister: High-Performance Equational Deduction",
+ journal = JAR,
+ volume = 18,
+ number = 2,
+ pages = {265--270},
+ year = 1997}
+
+@book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman},
+title={Introduction to Automata Theory, Languages, and Computation.},
+publisher={Addison-Wesley},year=1979}
+
+@Article{haskell-report,
+ author = {Paul Hudak and Simon Peyton Jones and Philip Wadler},
+ title = {Report on the Programming Language {Haskell}: A
+ Non-strict, Purely Functional Language},
+ journal = SIGPLAN,
+ year = 1992,
+ volume = 27,
+ number = 5,
+ month = May,
+ note = {Version 1.2}}
+
+@Article{haskell-tutorial,
+ author = {Paul Hudak and Joseph H. Fasel},
+ title = {A Gentle Introduction to {Haskell}},
+ journal = SIGPLAN,
+ year = 1992,
+ volume = 27,
+ number = 5,
+ month = May}
+
+@inproceedings{sine,
+ author = "Kry\v{s}tof Hoder and Andrei Voronkov",
+ title = "Sine Qua Non for Large Theory Reasoning",
+ booktitle = {Automated Deduction --- CADE-23},
+ publisher = Springer,
+ series = LNCS,
+ volume = 6803,
+ pages = "299--314",
+ editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
+ year = 2011}
+
+@book{Hudak-Haskell,author={Paul Hudak},
+title={The Haskell School of Expression},publisher=CUP,year=2000}
+
+@article{huet75,
+ author = {G. P. Huet},
+ title = {A Unification Algorithm for Typed $\lambda$-Calculus},
+ journal = TCS,
+ volume = 1,
+ year = 1975,
+ pages = {27-57}}
+
+@article{huet78,
+ author = {G. P. Huet and B. Lang},
+ title = {Proving and Applying Program Transformations Expressed with
+ Second-Order Patterns},
+ journal = acta,
+ volume = 11,
+ year = 1978,
+ pages = {31-55}}
+
+@inproceedings{huet88,
+ author = {G{\'e}rard Huet},
+ title = {Induction Principles Formalized in the {Calculus of
+ Constructions}},
+ booktitle = {Programming of Future Generation Computers},
+ editor = {K. Fuchi and M. Nivat},
+ year = 1988,
+ pages = {205-216},
+ publisher = {Elsevier}}
+
+@Book{Huth-Ryan-book,
+ author = {Michael Huth and Mark Ryan},
+ title = {Logic in Computer Science. Modelling and reasoning about systems},
+ publisher = CUP,
+ year = 2000}
+
+@InProceedings{Harrison:1996:MizarHOL,
+ author = {J. Harrison},
+ title = {A {Mizar} Mode for {HOL}},
+ pages = {203--220},
+ crossref = {tphols96}}
+
+@misc{metis,
+ author = "Joe Hurd",
+ title = "Metis Theorem Prover",
+ note = "\url{http://www.gilith.com/software/metis/}"}
+
+%J
+
+@article{haskell-revised-report,
+ author = {Simon {Peyton Jones} and others},
+ title = {The {Haskell} 98 Language and Libraries: The Revised Report},
+ journal = {Journal of Functional Programming},
+ volume = 13,
+ number = 1,
+ pages = {0--255},
+ month = {Jan},
+ year = 2003,
+ note = {\url{http://www.haskell.org/definition/}}}
+
+@book{jackson-2006,
+ author = "Daniel Jackson",
+ title = "Software Abstractions: Logic, Language, and Analysis",
+ publisher = MIT,
+ year = 2006}
+
+%K
+
+@InProceedings{kammueller-locales,
+ author = {Florian Kamm{\"u}ller and Markus Wenzel and
+ Lawrence C. Paulson},
+ title = {Locales: A Sectioning Concept for {Isabelle}},
+ crossref = {tphols99}}
+
+@book{Knuth3-75,
+ author={Donald E. Knuth},
+ title={The Art of Computer Programming, Volume 3: Sorting and Searching},
+ publisher={Addison-Wesley},
+ year=1975}
+
+@Article{korf85,
+ author = {R. E. Korf},
+ title = {Depth-First Iterative-Deepening: an Optimal Admissible
+ Tree Search},
+ journal = AI,
+ year = 1985,
+ volume = 27,
+ pages = {97-109}}
+
+@inproceedings{korovin-2009,
+ title = "Instantiation-Based Automated Reasoning: From Theory to Practice",
+ author = "Konstantin Korovin",
+ editor = "Renate A. Schmidt",
+ booktitle = {Automated Deduction --- CADE-22},
+ series = "LNAI",
+ volume = {5663},
+ pages = "163--166",
+ year = 2009,
+ publisher = "Springer"}
+
+@inproceedings{korovin-sticksel-2010,
+ author = {Konstantin Korovin and
+ Christoph Sticksel},
+ title = {{iP}rover-{E}q: An Instantiation-Based Theorem Prover with Equality},
+ pages = {196--202},
+ booktitle={Automated Reasoning: IJCAR 2010},
+ editor={J. Giesl and R. H\"ahnle},
+ publisher = Springer,
+ series = LNCS,
+ volume = 6173,
+ year = 2010}
+
+@InProceedings{krauss2006,
+ author = {Alexander Krauss},
+ title = {Partial Recursive Functions in {Higher-Order Logic}},
+ crossref = {ijcar2006},
+ pages = {589--603}}
+
+@PhdThesis{krauss_phd,
+ author = {Alexander Krauss},
+ title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
+ school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
+ year = {2009},
+ address = {Germany}
+}
+
+@manual{isabelle-function,
+ author = {Alexander Krauss},
+ title = {Defining Recursive Functions in {Isabelle/HOL}},
+ institution = TUM,
+ note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
+}
+
+@Book{kunen80,
+ author = {Kenneth Kunen},
+ title = {Set Theory: An Introduction to Independence Proofs},
+ publisher = NH,
+ year = 1980}
+
+%L
+
+@manual{OCaml,
+ author = {Xavier Leroy and others},
+ title = {The Objective Caml system -- Documentation and user's manual},
+ note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}}
+
+@incollection{lochbihler-2010,
+ title = "Coinduction",
+ author = "Andreas Lochbihler",
+ booktitle = "The Archive of Formal Proofs",
+ editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
+ publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
+ month = "Feb.",
+ year = 2010}
+
+@book{loveland-78,
+ author = "D. W. Loveland",
+ title = "Automated Theorem Proving: A Logical Basis",
+ year = 1978,
+ publisher = "North-Holland Publishing Co."}
+
+@InProceedings{lowe-fdr,
+ author = {Gavin Lowe},
+ title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
+ Protocol using {CSP} and {FDR}},
+ booktitle = {Tools and Algorithms for the Construction and Analysis
+ of Systems: second international workshop, TACAS '96},
+ editor = {T. Margaria and B. Steffen},
+ series = {LNCS 1055},
+ year = 1996,
+ publisher = {Springer},
+ pages = {147-166}}
+
+%M
+
+@Article{mw81,
+ author = {Zohar Manna and Richard Waldinger},
+ title = {Deductive Synthesis of the Unification Algorithm},
+ journal = SCP,
+ year = 1981,
+ volume = 1,
+ number = 1,
+ pages = {5-48}}
+
+@InProceedings{martin-nipkow,
+ author = {Ursula Martin and Tobias Nipkow},
+ title = {Ordered Rewriting and Confluence},
+ crossref = {cade10},
+ pages = {366-380}}
+
+@book{martinlof84,
+ author = {Per Martin-L{\"o}f},
+ title = {Intuitionistic type theory},
+ year = 1984,
+ publisher = {Bibliopolis}}
+
+@incollection{melham89,
+ author = {Thomas F. Melham},
+ title = {Automating Recursive Type Definitions in Higher Order
+ Logic},
+ pages = {341-386},
+ crossref = {birtwistle89}}
+
+@Article{Miller:1991,
+ author = {Dale Miller},
+ title = {A Logic Programming Language with Lambda-Abstraction, Function Variables,
+ and Simple Unification},
+ journal = {Journal of Logic and Computation},
+ year = 1991,
+ volume = 1,
+ number = 4
+}
+
+@Article{miller-mixed,
+ Author = {Dale Miller},
+ Title = {Unification Under a Mixed Prefix},
+ journal = JSC,
+ volume = 14,
+ number = 4,
+ pages = {321-358},
+ Year = 1992}
+
+@Article{milner78,
+ author = {Robin Milner},
+ title = {A Theory of Type Polymorphism in Programming},
+ journal = "J. Comp.\ Sys.\ Sci.",
+ year = 1978,
+ volume = 17,
+ pages = {348-375}}
+
+@TechReport{milner-ind,
+ author = {Robin Milner},
+ title = {How to Derive Inductions in {LCF}},
+ institution = Edinburgh,
+ year = 1980,
+ type = {note}}
+
+@Article{milner-coind,
+ author = {Robin Milner and Mads Tofte},
+ title = {Co-induction in Relational Semantics},
+ journal = TCS,
+ year = 1991,
+ volume = 87,
+ pages = {209-220}}
+
+@Book{milner89,
+ author = {Robin Milner},
+ title = {Communication and Concurrency},
+ publisher = Prentice,
+ year = 1989}
+
+@book{SML,author="Robin Milner and Mads Tofte and Robert Harper",
+title="The Definition of Standard ML",publisher=MIT,year=1990}
+
+@PhdThesis{monahan84,
+ author = {Brian Q. Monahan},
+ title = {Data Type Proofs using Edinburgh {LCF}},
+ school = {University of Edinburgh},
+ year = 1984}
+
+@article{MuellerNvOS99,
+author=
+{Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
+title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191--223}}
+
+@Manual{Muzalewski:Mizar,
+ title = {An Outline of {PC} {Mizar}},
+ author = {Micha{\l} Muzalewski},
+ organization = {Fondation of Logic, Mathematics and Informatics
+ --- Mizar Users Group},
+ year = 1993,
+ note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}}
+}
+
+%N
+
+@InProceedings{NaraschewskiW-TPHOLs98,
+ author = {Wolfgang Naraschewski and Markus Wenzel},
+ title =
+{Object-Oriented Verification based on Record Subtyping in
+ Higher-Order Logic},
+ crossref = {tphols98}}
+
+@inproceedings{nazareth-nipkow,
+ author = {Dieter Nazareth and Tobias Nipkow},
+ title = {Formal Verification of Algorithm {W}: The Monomorphic Case},
+ crossref = {tphols96},
+ pages = {331-345},
+ year = 1996}
+
+@Article{needham-schroeder,
+ author = "Roger M. Needham and Michael D. Schroeder",
+ title = "Using Encryption for Authentication in Large Networks
+ of Computers",
+ journal = cacm,
+ volume = 21,
+ number = 12,
+ pages = "993-999",
+ month = dec,
+ year = 1978}
+
+@inproceedings{nipkow-W,
+ author = {Wolfgang Naraschewski and Tobias Nipkow},
+ title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
+ booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96},
+ editor = {E. Gim{\'e}nez and C. Paulin-Mohring},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1512,
+ pages = {317-332},
+ year = 1998}
+
+@InCollection{nipkow-sorts93,
+ author = {T. Nipkow},
+ title = {Order-Sorted Polymorphism in {Isabelle}},
+ booktitle = {Logical Environments},
+ publisher = CUP,
+ year = 1993,
+ editor = {G. Huet and G. Plotkin},
+ pages = {164--188}
+}
+
+@Misc{nipkow-types93,
+ author = {Tobias Nipkow},
+ title = {Axiomatic Type Classes (in {I}sabelle)},
+ howpublished = {Presentation at the workshop \emph{Types for Proof and Programs}, Nijmegen},
+ year = 1993
+}
+
+@inproceedings{Nipkow-CR,
+ author = {Tobias Nipkow},
+ title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
+ booktitle = {Automated Deduction --- CADE-13},
+ editor = {M. McRobbie and J.K. Slaney},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1104,
+ pages = {733-747},
+ year = 1996}
+
+% WAS Nipkow-LICS-93
+@InProceedings{nipkow-patterns,
+ title = {Functional Unification of Higher-Order Patterns},
+ author = {Tobias Nipkow},
+ pages = {64-74},
+ crossref = {lics8},
+ url = {\url{ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html}},
+ keywords = {unification}}
+
+@article{nipkow-IMP,
+ author = {Tobias Nipkow},
+ title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
+ journal = FAC,
+ volume = 10,
+ pages = {171-186},
+ year = 1998}
+
+@inproceedings{Nipkow-TYPES02,
+ author = {Tobias Nipkow},
+ title = {{Structured Proofs in Isar/HOL}},
+ booktitle = {Types for Proofs and Programs (TYPES 2002)},
+ editor = {H. Geuvers and F. Wiedijk},
+ year = 2003,
+ publisher = Springer,
+ series = LNCS,
+ volume = 2646,
+ pages = {259-278}}
+
+@manual{isabelle-HOL,
+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ title = {{Isabelle}'s Logics: {HOL}},
+ institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
+ M{\"u}nchen and Computer Laboratory, University of Cambridge},
+ note = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
+
+@article{nipkow-prehofer,
+ author = {Tobias Nipkow and Christian Prehofer},
+ title = {Type Reconstruction for Type Classes},
+ journal = JFP,
+ volume = 5,
+ number = 2,
+ year = 1995,
+ pages = {201-224}}
+
+@InProceedings{Nipkow-Prehofer:1993,
+ author = {T. Nipkow and C. Prehofer},
+ title = {Type checking type classes},
+ booktitle = {ACM Symp.\ Principles of Programming Languages},
+ year = 1993
+}
+
+@Book{isa-tutorial,
+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ title = {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic},
+ publisher = Springer,
+ year = 2002,
+ series = LNCS,
+ volume = 2283}
+
+@Article{noel,
+ author = {Philippe No{\"e}l},
+ title = {Experimenting with {Isabelle} in {ZF} Set Theory},
+ journal = JAR,
+ volume = 10,
+ number = 1,
+ pages = {15-58},
+ year = 1993}
+
+@book{nordstrom90,
+ author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith},
+ title = {Programming in {Martin-L{\"o}f}'s Type Theory. An
+ Introduction},
+ publisher = {Oxford University Press},
+ year = 1990}
+
+%O
+
+@TechReport{scala-overview-tech-report,
+ author = {Martin Odersky and al.},
+ title = {An Overview of the Scala Programming Language},
+ institution = {EPFL Lausanne, Switzerland},
+ year = 2004,
+ number = {IC/2004/64}
+}
+
+@Article{Oppen:1980,
+ author = {D. C. Oppen},
+ title = {Pretty Printing},
+ journal = {ACM Transactions on Programming Languages and Systems},
+ year = 1980,
+ volume = 2,
+ number = 4}
+
+@Manual{pvs-language,
+ title = {The {PVS} specification language},
+ author = {S. Owre and N. Shankar and J. M. Rushby},
+ organization = {Computer Science Laboratory, SRI International},
+ address = {Menlo Park, CA},
+ note = {Beta release},
+ year = 1993,
+ month = apr,
+ url = {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}}
+
+%P
+
+% replaces paulin92
+@InProceedings{paulin-tlca,
+ author = {Christine Paulin-Mohring},
+ title = {Inductive Definitions in the System {Coq}: Rules and
+ Properties},
+ crossref = {tlca93},
+ pages = {328-345}}
+
+@InProceedings{paulson-CADE,
+ author = {Lawrence C. Paulson},
+ title = {A Fixedpoint Approach to Implementing (Co)Inductive
+ Definitions},
+ pages = {148-161},
+ crossref = {cade12}}
+
+@InProceedings{paulson-COLOG,
+ author = {Lawrence C. Paulson},
+ title = {A Formulation of the Simple Theory of Types (for
+ {Isabelle})},
+ pages = {246-274},
+ crossref = {colog88},
+ url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}
+
+@Article{paulson-coind,
+ author = {Lawrence C. Paulson},
+ title = {Mechanizing Coinduction and Corecursion in Higher-Order
+ Logic},
+ journal = JLC,
+ year = 1997,
+ volume = 7,
+ number = 2,
+ month = mar,
+ pages = {175-204}}
+
+@manual{isabelle-intro,
+ author = {Lawrence C. Paulson},
+ title = {Old Introduction to {Isabelle}},
+ institution = CUCL,
+ note = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}}
+
+@manual{isabelle-logics,
+ author = {Lawrence C. Paulson},
+ title = {{Isabelle's} Logics},
+ institution = CUCL,
+ note = {\url{http://isabelle.in.tum.de/doc/logics.pdf}}}
+
+@manual{isabelle-ref,
+ author = {Lawrence C. Paulson},
+ title = {The Old {Isabelle} Reference Manual},
+ institution = CUCL,
+ note = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}}
+
+@manual{isabelle-ZF,
+ author = {Lawrence C. Paulson},
+ title = {{Isabelle}'s Logics: {FOL} and {ZF}},
+ institution = CUCL,
+ note = {\url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}}}
+
+@article{paulson-found,
+ author = {Lawrence C. Paulson},
+ title = {The Foundation of a Generic Theorem Prover},
+ journal = JAR,
+ volume = 5,
+ number = 3,
+ pages = {363-397},
+ year = 1989,
+ url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}}
+
+%replaces paulson-final
+@Article{paulson-mscs,
+ author = {Lawrence C. Paulson},
+ title = {Final Coalgebras as Greatest Fixed Points
+ in {ZF} Set Theory},
+ journal = {Mathematical Structures in Computer Science},
+ year = 1999,
+ volume = 9,
+ number = 5,
+ pages = {545-567}}
+
+@InCollection{paulson-generic,
+ author = {Lawrence C. Paulson},
+ title = {Generic Automatic Proof Tools},
+ crossref = {wos-fest},
+ chapter = 3}
+
+@Article{paulson-gr,
+ author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
+ title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of
+ Choice},
+ journal = JAR,
+ year = 1996,
+ volume = 17,
+ number = 3,
+ month = dec,
+ pages = {291-323}}
+
+@InCollection{paulson-fixedpt-milner,
+ author = {Lawrence C. Paulson},
+ title = {A Fixedpoint Approach to (Co)inductive and
+ (Co)datatype Definitions},
+ pages = {187-211},
+ crossref = {milner-fest}}
+
+@book{milner-fest,
+ title = {Proof, Language, and Interaction:
+ Essays in Honor of {Robin Milner}},
+ booktitle = {Proof, Language, and Interaction:
+ Essays in Honor of {Robin Milner}},
+ publisher = MIT,
+ year = 2000,
+ editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}}
+
+@InCollection{paulson-handbook,
+ author = {Lawrence C. Paulson},
+ title = {Designing a Theorem Prover},
+ crossref = {handbk-lics2},
+ pages = {415-475}}
+
+@Book{paulson-isa-book,
+ author = {Lawrence C. Paulson},
+ title = {Isabelle: A Generic Theorem Prover},
+ publisher = {Springer},
+ year = 1994,
+ note = {LNCS 828}}
+
+@Book{isabelle-hol-book,
+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
+ publisher = {Springer},
+ year = 2002,
+ note = {LNCS 2283}}
+
+@InCollection{paulson-markt,
+ author = {Lawrence C. Paulson},
+ title = {Tool Support for Logics of Programs},
+ booktitle = {Mathematical Methods in Program Development:
+ Summer School Marktoberdorf 1996},
+ publisher = {Springer},
+ pages = {461-498},
+ year = {Published 1997},
+ editor = {Manfred Broy},
+ series = {NATO ASI Series F}}
+
+%replaces Paulson-ML and paulson91
+@book{paulson-ml2,
+ author = {Lawrence C. Paulson},
+ title = {{ML} for the Working Programmer},
+ year = 1996,
+ edition = {2nd},
+ publisher = CUP}
+
+@article{paulson-natural,
+ author = {Lawrence C. Paulson},
+ title = {Natural Deduction as Higher-order Resolution},
+ journal = JLP,
+ volume = 3,
+ pages = {237-258},
+ year = 1986,
+ url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}}
+
+@Article{paulson-set-I,
+ author = {Lawrence C. Paulson},
+ title = {Set Theory for Verification: {I}. {From}
+ Foundations to Functions},
+ journal = JAR,
+ volume = 11,
+ number = 3,
+ pages = {353-389},
+ year = 1993,
+ url = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/set-I.pdf}}}
+
+@Article{paulson-set-II,
+ author = {Lawrence C. Paulson},
+ title = {Set Theory for Verification: {II}. {Induction} and
+ Recursion},
+ journal = JAR,
+ volume = 15,
+ number = 2,
+ pages = {167-215},
+ year = 1995,
+ url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}}
+
+@article{paulson85,
+ author = {Lawrence C. Paulson},
+ title = {Verifying the Unification Algorithm in {LCF}},
+ journal = SCP,
+ volume = 5,
+ pages = {143-170},
+ year = 1985}
+
+%replaces Paulson-LCF
+@book{paulson87,
+ author = {Lawrence C. Paulson},
+ title = {Logic and Computation: Interactive proof with Cambridge
+ LCF},
+ year = 1987,
+ publisher = CUP}
+
+@incollection{paulson700,
+ author = {Lawrence C. Paulson},
+ title = {{Isabelle}: The Next 700 Theorem Provers},
+ crossref = {odifreddi90},
+ pages = {361-386},
+ url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}}
+
+% replaces paulson-ns and paulson-security
+@Article{paulson-jcs,
+ author = {Lawrence C. Paulson},
+ title = {The Inductive Approach to Verifying Cryptographic Protocols},
+ journal = JCS,
+ year = 1998,
+ volume = 6,
+ pages = {85-128}}
+
+@Article{paulson-tls,
+ author = {Lawrence C. Paulson},
+ title = {Inductive Analysis of the {Internet} Protocol {TLS}},
+ journal = TISSEC,
+ month = aug,
+ year = 1999,
+ volume = 2,
+ number = 3,
+ pages = {332-351}}
+
+@Article{paulson-yahalom,
+ author = {Lawrence C. Paulson},
+ title = {Relations Between Secrets:
+ Two Formal Analyses of the {Yahalom} Protocol},
+ journal = JCS,
+ volume = 9,
+ number = 3,
+ pages = {197-216},
+ year = 2001}}
+
+@article{pelletier86,
+ author = {F. J. Pelletier},
+ title = {Seventy-five Problems for Testing Automatic Theorem
+ Provers},
+ journal = JAR,
+ volume = 2,
+ pages = {191-216},
+ year = 1986,
+ note = {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}
+
+@InCollection{pitts93,
+ author = {A. Pitts},
+ title = {The {HOL} Logic},
+ editor = {M. J. C. Gordon and T. F. Melham},
+ booktitle = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
+ pages = {191--232},
+ publisher = CUP,
+ year = 1993}
+
+@Article{pitts94,
+ author = {Andrew M. Pitts},
+ title = {A Co-induction Principle for Recursively Defined Domains},
+ journal = TCS,
+ volume = 124,
+ pages = {195-219},
+ year = 1994}
+
+@Article{plaisted90,
+ author = {David A. Plaisted},
+ title = {A Sequent-Style Model Elimination Strategy and a Positive
+ Refinement},
+ journal = JAR,
+ year = 1990,
+ volume = 6,
+ number = 4,
+ pages = {389-402}}
+
+%Q
+
+@Article{quaife92,
+ author = {Art Quaife},
+ title = {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set
+ Theory},
+ journal = JAR,
+ year = 1992,
+ volume = 8,
+ number = 1,
+ pages = {91-147}}
+
+%R
+
+@TechReport{rasmussen95,
+ author = {Ole Rasmussen},
+ title = {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
+ Experiment},
+ institution = {Computer Laboratory, University of Cambridge},
+ year = 1995,
+ number = 364,
+ month = may,
+ url = {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}}
+
+@Book{reeves90,
+ author = {Steve Reeves and Michael Clarke},
+ title = {Logic for Computer Science},
+ publisher = {Addison-Wesley},
+ year = 1990}
+
+@article{riazanov-voronkov-2002,
+ author = "Alexander Riazanov and Andrei Voronkov",
+ title = "The Design and Implementation of {Vampire}",
+ journal = "Journal of AI Communications",
+ year = 2002,
+ volume = 15,
+ number ="2/3",
+ pages = "91--110"}
+
+@book{Rosen-DMA,author={Kenneth H. Rosen},
+title={Discrete Mathematics and Its Applications},
+publisher={McGraw-Hill},year=1998}
+
+@InProceedings{Rudnicki:1992:MizarOverview,
+ author = {P. Rudnicki},
+ title = {An Overview of the {MIZAR} Project},
+ booktitle = {1992 Workshop on Types for Proofs and Programs},
+ year = 1992,
+ organization = {Chalmers University of Technology},
+ publisher = {Bastad}
+}
+
+%S
+
+@inproceedings{saaltink-fme,
+ author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
+ Dan Craigen and Irwin Meisels},
+ title = {An {EVES} Data Abstraction Example},
+ pages = {578-596},
+ crossref = {fme93}}
+
+@Article{Schroeder-Heister:1984,
+ author = {Peter Schroeder-Heister},
+ title = {A Natural Extension of Natural Deduction},
+ journal = {Journal of Symbolic Logic},
+ year = 1984,
+ volume = 49,
+ number = 4
+}
+
+@article{schulz-2002,
+ author = "Stephan Schulz",
+ title = "E---A Brainiac Theorem Prover",
+ journal = "Journal of AI Communications",
+ year = 2002,
+ volume = 15,
+ number ="2/3",
+ pages = "111--126"}
+
+@misc{sledgehammer-2009,
+ key = "Sledgehammer",
+ title = "The {S}ledgehammer: Let Automatic Theorem Provers
+Write Your {I}s\-a\-belle Scripts",
+ note = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/sledgehammer.html}"}
+
+@inproceedings{slind-tfl,
+ author = {Konrad Slind},
+ title = {Function Definition in Higher Order Logic},
+ crossref = {tphols96},
+ pages = {381-397}}
+
+@inproceedings{snark,
+ author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood},
+ title = {Deductive composition of astronomical software from subroutine libraries},
+ pages = "341--355",
+ crossref = {cade12}}
+
+@book{suppes72,
+ author = {Patrick Suppes},
+ title = {Axiomatic Set Theory},
+ year = 1972,
+ publisher = {Dover}}
+
+@inproceedings{sutcliffe-2000,
+ author = "Geoff Sutcliffe",
+ title = "System Description: {SystemOnTPTP}",
+ editor = "David McAllester",
+ booktitle = {Automated Deduction --- {CADE}-17 International Conference},
+ series = "Lecture Notes in Artificial Intelligence",
+ volume = {1831},
+ pages = "406--410",
+ year = 2000,
+ publisher = Springer}
+
+@misc{tofof,
+ author = "Geoff Sutcliffe",
+ title = "{ToFoF}",
+ note = "\url{http://www.cs.miami.edu/~tptp/ATPSystems/ToFoF/}"}
+
+@Article{Sutter:2005,
+ author = {H. Sutter},
+ title = {The Free Lunch Is Over --- A Fundamental Turn Toward Concurrency in Software},
+ journal = {Dr. Dobb's Journal},
+ year = 2005,
+ volume = 30,
+ number = 3}
+
+@InCollection{szasz93,
+ author = {Nora Szasz},
+ title = {A Machine Checked Proof that {Ackermann's} Function is not
+ Primitive Recursive},
+ crossref = {huet-plotkin93},
+ pages = {317-338}}
+
+@TechReport{Syme:1997:DECLARE,
+ author = {D. Syme},
+ title = {{DECLARE}: A Prototype Declarative Proof System for Higher Order Logic},
+ institution = {University of Cambridge Computer Laboratory},
+ year = 1997,
+ number = 416
+}
+
+@PhdThesis{Syme:1998:thesis,
+ author = {D. Syme},
+ title = {Declarative Theorem Proving for Operational Semantics},
+ school = {University of Cambridge},
+ year = 1998,
+ note = {Submitted}
+}
+
+@InProceedings{Syme:1999:TPHOL,
+ author = {D. Syme},
+ title = {Three Tactic Theorem Proving},
+ crossref = {tphols99}}
+
+%T
+
+@book{takeuti87,
+ author = {G. Takeuti},
+ title = {Proof Theory},
+ year = 1987,
+ publisher = NH,
+ edition = {2nd}}
+
+@Book{thompson91,
+ author = {Simon Thompson},
+ title = {Type Theory and Functional Programming},
+ publisher = {Addison-Wesley},
+ year = 1991}
+
+@book{Thompson-Haskell,author={Simon Thompson},
+title={Haskell: The Craft of Functional Programming},
+publisher={Addison-Wesley},year=1999}
+
+@misc{kodkod-2009,
+ author = "Emina Torlak",
+ title = {Kodkod: Constraint Solver for Relational Logic},
+ note = "\url{http://alloy.mit.edu/kodkod/}"}
+
+@misc{kodkod-2009-options,
+ author = "Emina Torlak",
+ title = "Kodkod {API}: Class {Options}",
+ note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"}
+
+@inproceedings{torlak-jackson-2007,
+ title = "Kodkod: A Relational Model Finder",
+ author = "Emina Torlak and Daniel Jackson",
+ editor = "Orna Grumberg and Michael Huth",
+ booktitle = "TACAS 2007",
+ series = LNCS,
+ volume = {4424},
+ pages = "632--647",
+ year = 2007,
+ publisher = Springer}
+
+@unpublished{traytel-berghofer-nipkow-2011,
+ author = {D. Traytel and S. Berghofer and T. Nipkow},
+ title = {Extending Hindley-Milner Type Inference with Coercive
+ Subtyping (long version)},
+ year = 2011,
+ note = {Submitted,
+ \url{http://isabelle.in.tum.de/doc/implementation.pdf}}},
+}
+
+@Unpublished{Trybulec:1993:MizarFeatures,
+ author = {A. Trybulec},
+ title = {Some Features of the {Mizar} Language},
+ note = {Presented at a workshop in Turin, Italy},
+ year = 1993
+}
+
+%V
+
+@Unpublished{voelker94,
+ author = {Norbert V{\"o}lker},
+ title = {The Verification of a Timer Program using {Isabelle/HOL}},
+ url = {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}},
+ year = 1994,
+ month = aug}
+
+%W
+
+@inproceedings{wadler89how,
+ author = {P. Wadler and S. Blott},
+ title = {How to make ad-hoc polymorphism less ad-hoc},
+ booktitle = {ACM Symp.\ Principles of Programming Languages},
+ year = 1989
+}
+
+@phdthesis{weber-2008,
+ author = "Tjark Weber",
+ title = "SAT-Based Finite Model Generation for Higher-Order Logic",
+ school = {Dept.\ of Informatics, T.U. M\"unchen},
+ type = "{Ph.D.}\ thesis",
+ year = 2008}
+
+@Misc{x-symbol,
+ author = {Christoph Wedler},
+ title = {Emacs package ``{X-Symbol}''},
+ note = {\url{http://x-symbol.sourceforge.net}}
+}
+
+@misc{weidenbach-et-al-2009,
+ author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski",
+ title = "{SPASS} Version 3.5",
+ note = {\url{http://www.spass-prover.org/publications/spass.pdf}}}
+
+@manual{isabelle-sys,
+ author = {Markus Wenzel and Stefan Berghofer},
+ title = {The {Isabelle} System Manual},
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}
+
+@manual{isabelle-isar-ref,
+ author = {Makarius Wenzel},
+ title = {The {Isabelle/Isar} Reference Manual},
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
+
+@manual{isabelle-implementation,
+ author = {Makarius Wenzel},
+ title = {The {Isabelle/Isar} Implementation},
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+
+@InProceedings{Wenzel:1999:TPHOL,
+ author = {Markus Wenzel},
+ title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
+ crossref = {tphols99}}
+
+@InProceedings{Wenzel:1997:TPHOL,
+ author = {Markus Wenzel},
+ title = {Type Classes and Overloading in Higher-Order Logic},
+ crossref = {tphols97}}
+
+@phdthesis{Wenzel-PhD,
+ author={Markus Wenzel},
+ title={Isabelle/Isar --- a versatile environment for human-readable formal proof documents},
+ school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
+ year=2002,
+ note = {\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}}}
+
+@Article{Wenzel-Wiedijk:2002,
+ author = {Freek Wiedijk and Markus Wenzel},
+ title = {A comparison of the mathematical proof languages {Mizar} and {Isar}.},
+ journal = {Journal of Automated Reasoning},
+ year = 2002,
+ volume = 29,
+ number = {3-4}
+}
+
+@InCollection{Wenzel-Paulson:2006,
+ author = {Markus Wenzel and Lawrence C. Paulson},
+ title = {{Isabelle/Isar}},
+ booktitle = {The Seventeen Provers of the World},
+ year = 2006,
+ editor = {F. Wiedijk},
+ series = {LNAI 3600}
+}
+
+@InCollection{Wenzel:2006:Festschrift,
+ author = {Makarius Wenzel},
+ title = {{Isabelle/Isar} --- a generic framework for human-readable proof documents},
+ booktitle = {From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec},
+ publisher = {University of Bia{\l}ystok},
+ year = 2007,
+ editor = {R. Matuszewski and A. Zalewska},
+ volume = {10(23)},
+ series = {Studies in Logic, Grammar, and Rhetoric},
+ note = {\url{http://www.in.tum.de/~wenzelm/papers/isar-framework.pdf}}
+}
+
+@InProceedings{Wenzel-Chaieb:2007b,
+ author = {Makarius Wenzel and Amine Chaieb},
+ title = {{SML} with antiquotations embedded into {Isabelle/Isar}},
+ booktitle = {Workshop on Programming Languages for Mechanized Mathematics
+ (satellite of CALCULEMUS 2007). Hagenberg, Austria},
+ editor = {Jacques Carette and Freek Wiedijk},
+ month = {June},
+ year = {2007}
+}
+
+@InProceedings{Wenzel:2009,
+ author = {M. Wenzel},
+ title = {Parallel Proof Checking in {Isabelle/Isar}},
+ booktitle = {ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009)},
+ year = 2009,
+ editor = {Dos Reis, G. and L. Th\'ery},
+ publisher = {ACM Digital Library}}
+
+@book{principia,
+ author = {A. N. Whitehead and B. Russell},
+ title = {Principia Mathematica},
+ year = 1962,
+ publisher = CUP,
+ note = {Paperback edition to *56,
+ abridged from the 2nd edition (1927)}}
+
+@Misc{Wiedijk:1999:Mizar,
+ author = {Freek Wiedijk},
+ title = {Mizar: An Impression},
+ howpublished = {Unpublished paper},
+ year = 1999,
+ note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz}}
+}
+
+@Misc{Wiedijk:2000:MV,
+ author = {Freek Wiedijk},
+ title = {The Mathematical Vernacular},
+ howpublished = {Unpublished paper},
+ year = 2000,
+ note = {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}}
+}
+
+@misc{wikipedia-2009-aa-trees,
+ key = "Wikipedia",
+ title = "Wikipedia: {AA} Tree",
+ note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
+
+@book{winskel93,
+ author = {Glynn Winskel},
+ title = {The Formal Semantics of Programming Languages},
+ publisher = MIT,year=1993}
+
+@InCollection{wos-bledsoe,
+ author = {Larry Wos},
+ title = {Automated Reasoning and {Bledsoe's} Dream for the Field},
+ crossref = {bledsoe-fest},
+ pages = {297-342}}
+
+@InProceedings{Zammit:1999:TPHOL,
+ author = {Vincent Zammit},
+ title = {On the Implementation of an Extensible Declarative Proof Language},
+ crossref = {tphols99}}
+
+%Z
+
+@misc{z3,
+ key = "Z3",
+ title = "Z3: An Efficient {SMT} Solver",
+ note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"}
+
+
+% CROSS REFERENCES
+
+@book{handbk-lics2,
+ editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
+ title = {Handbook of Logic in Computer Science},
+ booktitle = {Handbook of Logic in Computer Science},
+ publisher = {Oxford University Press},
+ year = 1992,
+ volume = 2}
+
+@book{types93,
+ editor = {Henk Barendregt and Tobias Nipkow},
+ title = TYPES # {: International Workshop {TYPES '93}},
+ booktitle = TYPES # {: International Workshop {TYPES '93}},
+ year = {published 1994},
+ publisher = {Springer},
+ series = {LNCS 806}}
+
+@book{barwise-handbk,
+ editor = {J. Barwise},
+ title = {Handbook of Mathematical Logic},
+ booktitle = {Handbook of Mathematical Logic},
+ year = 1977,
+ publisher = NH}
+
+@Proceedings{tlca93,
+ title = {Typed Lambda Calculi and Applications},
+ booktitle = {Typed Lambda Calculi and Applications},
+ editor = {M. Bezem and J.F. Groote},
+ year = 1993,
+ publisher = {Springer},
+ series = {LNCS 664}}
+
+@book{birtwistle89,
+ editor = {Graham Birtwistle and P. A. Subrahmanyam},
+ title = {Current Trends in Hardware Verification and Automated
+ Theorem Proving},
+ booktitle = {Current Trends in Hardware Verification and Automated
+ Theorem Proving},
+ publisher = {Springer},
+ year = 1989}
+
+@book{bledsoe-fest,
+ title = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
+ booktitle = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
+ publisher = {Kluwer Academic Publishers},
+ year = 1991,
+ editor = {Robert S. Boyer}}
+
+@Proceedings{cade12,
+ editor = {Alan Bundy},
+ title = {Automated Deduction --- {CADE}-12
+ International Conference},
+ booktitle = {Automated Deduction --- {CADE}-12
+ International Conference},
+ year = 1994,
+ series = {LNAI 814},
+ publisher = {Springer}}
+
+@book{types94,
+ editor = {Peter Dybjer and Bengt Nordstr{{\"o}m} and Jan Smith},
+ title = TYPES # {: International Workshop {TYPES '94}},
+ booktitle = TYPES # {: International Workshop {TYPES '94}},
+ year = 1995,
+ publisher = {Springer},
+ series = {LNCS 996}}
+
+@book{huet-plotkin91,
+ editor = {{G{\'e}rard} Huet and Gordon Plotkin},
+ title = {Logical Frameworks},
+ booktitle = {Logical Frameworks},
+ publisher = CUP,
+ year = 1991}
+
+@book{huet-plotkin93,
+ editor = {{G{\'e}rard} Huet and Gordon Plotkin},
+ title = {Logical Environments},
+ booktitle = {Logical Environments},
+ publisher = CUP,
+ year = 1993}
+
+@Proceedings{hug93,
+ editor = {J. Joyce and C. Seger},
+ title = {Higher Order Logic Theorem Proving and Its
+ Applications: HUG '93},
+ booktitle = {Higher Order Logic Theorem Proving and Its
+ Applications: HUG '93},
+ year = {Published 1994},
+ publisher = {Springer},
+ series = {LNCS 780}}
+
+@proceedings{colog88,
+ editor = {P. Martin-L{\"o}f and G. Mints},
+ title = {COLOG-88: International Conference on Computer Logic},
+ booktitle = {COLOG-88: International Conference on Computer Logic},
+ year = {Published 1990},
+ publisher = {Springer},
+ organization = {Estonian Academy of Sciences},
+ address = {Tallinn},
+ series = {LNCS 417}}
+
+@book{odifreddi90,
+ editor = {P. Odifreddi},
+ title = {Logic and Computer Science},
+ booktitle = {Logic and Computer Science},
+ publisher = {Academic Press},
+ year = 1990}
+
+@proceedings{extensions91,
+ editor = {Peter Schroeder-Heister},
+ title = {Extensions of Logic Programming},
+ booktitle = {Extensions of Logic Programming},
+ year = 1991,
+ series = {LNAI 475},
+ publisher = {Springer}}
+
+@proceedings{cade10,
+ editor = {Mark E. Stickel},
+ title = {10th } # CADE,
+ booktitle = {10th } # CADE,
+ year = 1990,
+ publisher = {Springer},
+ series = {LNAI 449}}
+
+@Proceedings{lics8,
+ editor = {M. Vardi},
+ title = {Eighth Annual Symposium on Logic in Computer Science},
+ booktitle = {Eighth Annual Symposium on Logic in Computer Science},
+ publisher = IEEE,
+ year = 1993}
+
+@book{wos-fest,
+ title = {Automated Reasoning and its Applications:
+ Essays in Honor of {Larry Wos}},
+ booktitle = {Automated Reasoning and its Applications:
+ Essays in Honor of {Larry Wos}},
+ publisher = MIT,
+ year = 1997,
+ editor = {Robert Veroff}}
+
+@proceedings{fme93,
+ editor = {J. C. P. Woodcock and P. G. Larsen},
+ title = {FME '93: Industrial-Strength Formal Methods},
+ booktitle = {FME '93: Industrial-Strength Formal Methods},
+ year = 1993,
+ publisher = Springer,
+ series = LNCS,
+ volume = 670}
+
+@Proceedings{tphols96,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
+ editor = {J. von Wright and J. Grundy and J. Harrison},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1125,
+ year = 1996}
+
+@Proceedings{tphols97,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
+ editor = {Elsa L. Gunter and Amy Felty},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1275,
+ year = 1997}
+
+@Proceedings{tphols98,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
+ editor = {Jim Grundy and Malcom Newey},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1479,
+ year = 1998}
+
+@Proceedings{tphols99,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
+ editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
+ Paulin, C. and Thery, L.},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1690,
+ year = 1999}
+
+@Proceedings{tphols2000,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},
+ editor = {J. Harrison and M. Aagaard},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1869,
+ year = 2000}
+
+@Proceedings{tphols2001,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},
+ editor = {R. J. Boulton and P. B. Jackson},
+ publisher = Springer,
+ series = LNCS,
+ volume = 2152,
+ year = 2001}
+
+@Proceedings{ijcar2006,
+ title = {Automated Reasoning: {IJCAR} 2006},
+ booktitle = {Automated Reasoning: {IJCAR} 2006},
+ editor = {U. Furbach and N. Shankar},
+ publisher = Springer,
+ series = LNCS,
+ volume = 4130,
+ year = 2006}
+
+@Proceedings{tphols2007,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},
+ editor = {K. Schneider and J. Brandt},
+ publisher = Springer,
+ series = LNCS,
+ volume = 4732,
+ year = 2007}
+
+@Proceedings{tphols2008,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},
+ publisher = Springer,
+ series = LNCS,
+ year = 2008}
+% editor =
+% volume = 4732,
+
+@Proceedings{itp2010,
+ title = {Interactive Theorem Proving: {ITP}-10},
+ booktitle = {Interactive Theorem Proving: {ITP}-10},
+ editor = "Matt Kaufmann and Lawrence Paulson",
+ publisher = Springer,
+ series = LNCS,
+ year = 2010}
+
+@unpublished{classes_modules,
+ title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
+ author = {Stefan Wehr et. al.}
+}