doc-src/manual.bib

fixed off-by-one and return proper error code -- never underestimate the number of oddities in Perl

+
−% 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
+
−
+
−@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{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}
+
−
+
−@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{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,
+
−  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}
+
−
+
−@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},
+
−  publisher = "\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}
+
−}
+
−
+
−@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}
+
−
+
−@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}
+
−
+
−@misc{sine,
+
−  author = "Kry\v{s}tof Hoder",
+
−  title = "SInE (Sumo Inference Engine)",
+
−  note = "\url{http://www.cs.man.ac.uk/~hoderk/sine/}"}
+
−
+
−@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{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}
+
−
+
−@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}
+
−}
+
−
+
−@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}}
+
−
+
−@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}
+
−
+
−@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{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.}
+
−}