doc-src/manual.bib
author blanchet
Tue May 22 16:59:27 2012 +0200 (2012-05-22)
changeset 47955 a2a821abab83
parent 46643 a88bccd2b567
permissions -rw-r--r--
added one slice with configurable simplification turned off
     1 % BibTeX database for the Isabelle documentation
     2 
     3 %publishers
     4 @string{AP="Academic Press"}
     5 @string{CUP="Cambridge University Press"}
     6 @string{IEEE="IEEE Computer Society Press"}
     7 @string{LNCS="Lecture Notes in Computer Science"}
     8 @string{MIT="MIT Press"}
     9 @string{NH="North-Holland"}
    10 @string{Prentice="Prentice-Hall"}
    11 @string{PH="Prentice-Hall"}
    12 @string{Springer="Springer-Verlag"}
    13 
    14 %institutions
    15 @string{CUCL="Computer Laboratory, University of Cambridge"}
    16 @string{Edinburgh="Department of Computer Science, University of Edinburgh"}
    17 @string{TUM="Department of Informatics, Technical University of Munich"}
    18 
    19 %journals
    20 @string{AI="Artificial Intelligence"}
    21 @string{FAC="Formal Aspects of Computing"}
    22 @string{JAR="Journal of Automated Reasoning"}
    23 @string{JCS="Journal of Computer Security"}
    24 @string{JFP="Journal of Functional Programming"}
    25 @string{JLC="Journal of Logic and Computation"}
    26 @string{JLP="Journal of Logic Programming"}
    27 @string{JSC="Journal of Symbolic Computation"}
    28 @string{JSL="Journal of Symbolic Logic"}
    29 @string{PROYAL="Proceedings of the Royal Society of London"}
    30 @string{SIGPLAN="{SIGPLAN} Notices"}
    31 @string{TISSEC="ACM Transactions on Information and System Security"}
    32 
    33 %conferences
    34 @string{CADE="International Conference on Automated Deduction"}
    35 @string{POPL="Symposium on Principles of Programming Languages"}
    36 @string{TYPES="Types for Proofs and Programs"}
    37 
    38 
    39 %A
    40 
    41 @incollection{abramsky90,
    42   author	= {Samson Abramsky},
    43   title		= {The Lazy Lambda Calculus},
    44   pages		= {65-116},
    45   editor	= {David A. Turner},
    46   booktitle	= {Research Topics in Functional Programming},
    47   publisher	= {Addison-Wesley},
    48   year		= 1990}
    49 
    50 @Unpublished{abrial93,
    51   author	= {J. R. Abrial and G. Laffitte},
    52   title		= {Towards the Mechanization of the Proofs of Some Classical
    53 		  Theorems of Set Theory},
    54   note		= {preprint},
    55   year		= 1993,
    56   month		= Feb}
    57 
    58 @incollection{aczel77,
    59   author	= {Peter Aczel},
    60   title		= {An Introduction to Inductive Definitions},
    61   pages		= {739-782},
    62   crossref	= {barwise-handbk}}
    63 
    64 @Book{aczel88,
    65   author	= {Peter Aczel},
    66   title		= {Non-Well-Founded Sets},
    67   publisher	= {CSLI},
    68   year		= 1988}
    69 
    70 @inproceedings{Aehlig-Haftmann-Nipkow:2008:nbe,
    71   author =      {Klaus Aehlig and Florian Haftmann and Tobias Nipkow},
    72   title =       {A Compiled Implementation of Normalization by Evaluation},
    73   booktitle =   {TPHOLs '08: Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics},
    74   year =        {2008},
    75   isbn =        {978-3-540-71065-3},
    76   pages =       {352--367},
    77   publisher =   Springer,
    78   series =      LNCS,
    79   volume =      {5170},
    80   editor =      {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar}
    81 }
    82 
    83 @InProceedings{alf,
    84   author	= {Lena Magnusson and Bengt {Nordstr\"{o}m}},
    85   title		= {The {ALF} Proof Editor and Its Proof Engine},
    86   crossref	= {types93},
    87   pages		= {213-237}}
    88 
    89 @inproceedings{andersson-1993,
    90   author = "Arne Andersson",
    91   title = "Balanced Search Trees Made Simple",
    92   editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides",
    93   booktitle = "WADS 1993",
    94   series = LNCS,
    95   volume = {709},
    96   pages = "61--70",
    97   year = 1993,
    98   publisher = Springer}
    99 
   100 @book{andrews86,
   101   author	= "Peter Andrews",
   102   title		= "An Introduction to Mathematical Logic and Type Theory: to Truth
   103 through Proof",
   104   publisher	= AP,
   105   series	= "Computer Science and Applied Mathematics",
   106   year		= 1986}
   107 
   108 @InProceedings{Aspinall:2000:eProof,
   109   author = 	 {David Aspinall},
   110   title = 	 {Protocols for Interactive {e-Proof}},
   111   booktitle = 	 {Theorem Proving in Higher Order Logics (TPHOLs)},
   112   year =	 2000,
   113   note =	 {Unpublished work-in-progress paper,
   114                   \url{http://homepages.inf.ed.ac.uk/da/papers/drafts/eproof.ps.gz}}
   115 }
   116 
   117 @InProceedings{Aspinall:TACAS:2000,
   118   author = 	 {David Aspinall},
   119   title = 	 {{P}roof {G}eneral: A Generic Tool for Proof Development},
   120   booktitle = 	 {Tools and Algorithms for the Construction and Analysis of
   121                   Systems (TACAS)},
   122   year =	 2000,
   123   publisher	= Springer,
   124   series	= LNCS,
   125   volume	= 1785,
   126   pages = "38--42"
   127 }
   128 
   129 @Misc{isamode,
   130   author =	 {David Aspinall},
   131   title =	 {Isamode --- {U}sing {I}sabelle with {E}macs},
   132   note =	 {\url{http://homepages.inf.ed.ac.uk/da/Isamode/}}
   133 }
   134 
   135 @Misc{proofgeneral,
   136   author =	 {David Aspinall},
   137   title =	 {{P}roof {G}eneral},
   138   note =	 {\url{http://proofgeneral.inf.ed.ac.uk/}}
   139 }
   140 
   141 %B
   142 
   143 @inproceedings{backes-brown-2010,
   144   title = "Analytic Tableaux for Higher-Order Logic with Choice",
   145   author = "Julian Backes and Chad E. Brown",
   146   booktitle={Automated Reasoning: IJCAR 2010},
   147   editor={J. Giesl and R. H\"ahnle},
   148   publisher = Springer,
   149   series = LNCS,
   150   volume = 6173,
   151   pages = "76--90",
   152   year = 2010}
   153 
   154 @book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow},
   155 title="Term Rewriting and All That",publisher=CUP,year=1998}
   156 
   157 @manual{isabelle-locale,
   158   author        = {Clemens Ballarin},
   159   title         = {Tutorial to Locales and Locale Interpretation},
   160   institution   = TUM,
   161   note          = {\url{http://isabelle.in.tum.de/doc/locales.pdf}}
   162 }
   163 
   164 @InCollection{Barendregt-Geuvers:2001,
   165   author = 	 {H. Barendregt and H. Geuvers},
   166   title = 	 {Proof Assistants using Dependent Type Systems},
   167   booktitle = 	 {Handbook of Automated Reasoning},
   168   publisher =	 {Elsevier},
   169   year =	 2001,
   170   editor =	 {A. Robinson and A. Voronkov}
   171 }
   172 
   173 @inproceedings{cvc3,
   174   author    = {Clark Barrett and Cesare Tinelli},
   175   title     = {{CVC3}},
   176   booktitle = {CAV},
   177   editor    = {Werner Damm and Holger Hermanns},
   178   volume    = {4590},
   179   series    = LNCS,
   180   pages     = {298--302},
   181   publisher = {Springer},
   182   year      = {2007}
   183 }
   184 
   185 @incollection{basin91,
   186   author	= {David Basin and Matt Kaufmann},
   187   title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
   188 		   Comparison}, 
   189   crossref	= {huet-plotkin91},
   190   pages		= {89-119}}
   191 
   192 @Unpublished{HOL-Library,
   193   author =       {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and
   194                   Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and
   195                   Markus Wenzel},
   196   title =        {The Supplemental {Isabelle/HOL} Library},
   197   note =         {Part of the Isabelle distribution,
   198                   \url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
   199   year =         2002
   200 }
   201 
   202 @InProceedings{Bauer-Wenzel:2000:HB,
   203   author = 	 {Gertrud Bauer and Markus Wenzel},
   204   title = 	 {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
   205       {I}sabelle/{I}sar},
   206   booktitle = 	 {Types for Proofs and Programs: TYPES'99},
   207   editor =       {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
   208                   and Jan Smith},
   209   series =	 {LNCS},
   210   year =	 2000
   211 }
   212 
   213 @InProceedings{Bauer-Wenzel:2001,
   214   author =       {Gertrud Bauer and Markus Wenzel},
   215   title =        {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
   216   crossref =     {tphols2001}}
   217 
   218 @inproceedings{leo2,
   219   author = "Christoph Benzm{\"u}ller and Lawrence C. Paulson and Frank Theiss and Arnaud Fietzke",
   220   title = "{LEO-II}---A Cooperative Automatic Theorem Prover for Higher-Order Logic",
   221   editor = "Alessandro Armando and Peter Baumgartner and Gilles Dowek",
   222   booktitle = "Automated Reasoning: IJCAR 2008",
   223   publisher = Springer,
   224   series = LNCS,
   225   volume = 5195,
   226   pages = "162--170",
   227   year = 2008}
   228 
   229 @inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL,
   230     author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
   231     booktitle = {Theorem Proving in Higher Order Logics},
   232     pages = {131--146},
   233     title = {Turning Inductive into Equational Specifications},
   234     year = {2009}
   235 }
   236 
   237 @INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
   238   crossref        = "tphols2000",
   239   title           = "Proof terms for simply typed higher order logic",
   240   author          = "Stefan Berghofer and Tobias Nipkow",
   241   pages           = "38--52"}
   242 
   243 @inproceedings{berghofer-nipkow-2004,
   244   author = {Stefan Berghofer and Tobias Nipkow},
   245   title = {Random Testing in {I}sabelle/{HOL}},
   246   pages = {230--239},
   247   editor = "J. Cuellar and Z. Liu",
   248   booktitle = {{SEFM} 2004},
   249   publisher = IEEE,
   250   year = 2004}
   251 
   252 @InProceedings{Berghofer-Nipkow:2002,
   253   author =       {Stefan Berghofer and Tobias Nipkow},
   254   title =        {Executing Higher Order Logic},
   255   booktitle =    {Types for Proofs and Programs: TYPES'2000},
   256   editor =       {P. Callaghan and Z. Luo and J. McKinna and R. Pollack},
   257   series =       LNCS,
   258   publisher =    Springer,
   259   volume =       2277,
   260   year =         2002}
   261 
   262 @InProceedings{Berghofer-Wenzel:1999:TPHOL,
   263   author = 	 {Stefan Berghofer and Markus Wenzel},
   264   title = 	 {Inductive datatypes in {HOL} --- lessons learned in
   265                   {F}ormal-{L}ogic {E}ngineering},
   266   crossref =     {tphols99}}
   267 
   268 
   269 @InProceedings{Bezem-Coquand:2005,
   270   author = 	 {M.A. Bezem and T. Coquand},
   271   title = 	 {Automating {Coherent Logic}},
   272   booktitle = {LPAR-12},
   273   editor = 	 {G. Sutcliffe and A. Voronkov},
   274   volume = 	 3835,
   275   series = 	 LNCS,
   276   publisher = Springer}
   277 
   278 @book{Bird-Wadler,author="Richard Bird and Philip Wadler",
   279 title="Introduction to Functional Programming",publisher=PH,year=1988}
   280 
   281 @book{Bird-Haskell,author="Richard Bird",
   282 title="Introduction to Functional Programming using Haskell",
   283 publisher=PH,year=1998}
   284 
   285 @manual{isabelle-nitpick,
   286   author        = {Jasmin Christian Blanchette},
   287   title         = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle/{HOL}},
   288   institution   = TUM,
   289   note          = {\url{http://isabelle.in.tum.de/doc/nitpick.pdf}}
   290 }
   291 
   292 @manual{isabelle-sledgehammer,
   293   author        = {Jasmin Christian Blanchette},
   294   title         = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle/{HOL}},
   295   institution   = TUM,
   296   note          = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}
   297 }
   298 
   299 @inproceedings{blanchette-nipkow-2010,
   300   title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
   301   author = "Jasmin Christian Blanchette and Tobias Nipkow",
   302   crossref = {itp2010}}
   303 
   304 @inproceedings{why3,
   305   author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
   306   title = {{Why3}: Shepherd Your Herd of Provers},
   307   editor = "K. Rustan M. Leino and Micha\l{} Moskal",
   308   booktitle = {Boogie 2011},
   309   pages = "53--64",
   310   year = 2011
   311 }
   312 
   313 @inproceedings{alt-ergo,
   314   author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean and St\'ephane Lescuyer},
   315   title = {Implementing Polymorphism in {SMT} Solvers},
   316   booktitle = {SMT '08},
   317   pages = "1--5",
   318   publisher = "ACM",
   319   series = "ICPS",
   320   year = 2008,
   321   editor = {Clark Barrett and Leonardo de Moura}}
   322 % /BPR
   323 % and Domagoj Babic and Amit Goel
   324 
   325 @inproceedings{boehme-nipkow-2010,
   326   author={Sascha B\"ohme and Tobias Nipkow},
   327   title={Sledgehammer: Judgement Day},
   328   booktitle={Automated Reasoning: IJCAR 2010},
   329   editor={J. Giesl and R. H\"ahnle},
   330   publisher=Springer,
   331   series=LNCS,
   332   volume = 6173,
   333   pages = "107--121",
   334   year=2010}
   335 
   336 @Article{boyer86,
   337   author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
   338 		   Overbeek and Mark Stickel and Lawrence Wos},
   339   title		= {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}
   340 		   Axioms},
   341   journal	= JAR,
   342   year		= 1986,
   343   volume	= 2,
   344   number	= 3,
   345   pages		= {287-327}}
   346 
   347 @book{bm79,
   348   author	= {Robert S. Boyer and J Strother Moore},
   349   title		= {A Computational Logic},
   350   publisher	= {Academic Press},
   351   year		= 1979}
   352 
   353 @book{bm88book,
   354   author	= {Robert S. Boyer and J Strother Moore},
   355   title		= {A Computational Logic Handbook},
   356   publisher	= {Academic Press},
   357   year		= 1988}
   358 
   359 @inproceedings{satallax,
   360   author = "Chad E. Brown",
   361   title = "Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems",
   362   booktitle = {Automated Deduction --- CADE-23},
   363   publisher = Springer,
   364   series = LNCS,
   365   volume = 6803,
   366   pages = "147--161",
   367   editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
   368   year = 2011}
   369 
   370 @Article{debruijn72,
   371   author	= {N. G. de Bruijn},
   372   title		= {Lambda Calculus Notation with Nameless Dummies,
   373 	a Tool for Automatic Formula Manipulation,
   374 	with Application to the {Church-Rosser Theorem}},
   375   journal	= {Indag. Math.},
   376   volume	= 34,
   377   pages		= {381-392},
   378   year		= 1972}
   379 
   380 @InProceedings{bulwahnKN07,
   381   author   = {Lukas Bulwahn and Alexander Krauss and Tobias Nipkow},
   382   title    = {Finding Lexicographic Orders for Termination Proofs in {Isabelle/HOL}},
   383   crossref = {tphols2007},
   384   pages    = {38--53}
   385 }
   386 
   387 @InProceedings{bulwahn-et-al:2008:imperative,
   388   author   = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
   389   title    = {Imperative Functional Programming with {Isabelle/HOL}},
   390   crossref = {tphols2008},
   391 }
   392 %  pages    = {38--53}
   393 
   394 @Article{ban89,
   395   author	= {M. Burrows and M. Abadi and R. M. Needham},
   396   title		= {A Logic of Authentication},
   397   journal	= PROYAL,
   398   year		= 1989,
   399   volume	= 426,
   400   pages		= {233-271}}
   401 
   402 %C
   403 
   404 @InProceedings{Chaieb-Wenzel:2007,
   405   author = 	 {Amine Chaieb and Makarius Wenzel},
   406   title = 	 {Context aware Calculation and Deduction ---
   407                   Ring Equalities via {Gr\"obner Bases} in {Isabelle}},
   408   booktitle =	 {Towards Mechanized Mathematical Assistants (CALCULEMUS 2007)},
   409   editor =	 {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
   410   series =	 LNAI,
   411   volume =       4573,
   412   year =	 2007,
   413   publisher =	 Springer
   414 }
   415 
   416 @TechReport{camilleri92,
   417   author	= {J. Camilleri and T. F. Melham},
   418   title		= {Reasoning with Inductively Defined Relations in the
   419 		 {HOL} Theorem Prover},
   420   institution	= CUCL,
   421   year		= 1992,
   422   number	= 265,
   423   month		= Aug}
   424 
   425 @Book{charniak80,
   426   author	= {E. Charniak and C. K. Riesbeck and D. V. McDermott},
   427   title		= {Artificial Intelligence Programming},
   428   publisher	= {Lawrence Erlbaum Associates},
   429   year		= 1980}
   430 
   431 @article{church40,
   432   author	= "Alonzo Church",
   433   title		= "A Formulation of the Simple Theory of Types",
   434   journal	= JSL,
   435   year		= 1940,
   436   volume	= 5,
   437   pages		= "56-68"}
   438 
   439 @book{ClarkeGP-book,author="Edmund Clarke and Orna Grumberg and Doron Peled",
   440 title="Model Checking",publisher=MIT,year=1999}
   441 
   442 @PhdThesis{coen92,
   443   author	= {Martin D. Coen},
   444   title		= {Interactive Program Derivation},
   445   school	= {University of Cambridge},
   446   note		= {Computer Laboratory Technical Report 272},
   447   month		= nov,
   448   year		= 1992}
   449 
   450 @book{constable86,
   451   author	= {R. L. Constable and others},
   452   title		= {Implementing Mathematics with the Nuprl Proof
   453 		 Development System}, 
   454   publisher	= Prentice,
   455   year		= 1986}
   456 
   457 %D
   458 
   459 @Book{davey-priestley,
   460   author	= {B. A. Davey and H. A. Priestley},
   461   title		= {Introduction to Lattices and Order},
   462   publisher	= CUP,
   463   year		= 1990}
   464 
   465 @Book{devlin79,
   466   author	= {Keith J. Devlin},
   467   title		= {Fundamentals of Contemporary Set Theory},
   468   publisher	= {Springer},
   469   year		= 1979}
   470 
   471 @book{dummett,
   472   author	= {Michael Dummett},
   473   title		= {Elements of Intuitionism},
   474   year		= 1977,
   475   publisher	= {Oxford University Press}}
   476 
   477 @misc{yices,
   478   author    = {Bruno Dutertre and Leonardo de Moura},
   479   title     = {The {Yices} {SMT} Solver},
   480   howpublished = "\url{http://yices.csl.sri.com/tool-paper.pdf}",
   481   year = 2006}
   482 
   483 @incollection{dybjer91,
   484   author	= {Peter Dybjer},
   485   title		= {Inductive Sets and Families in {Martin-L{\"o}f's} Type
   486 		  Theory and Their Set-Theoretic Semantics}, 
   487   crossref	= {huet-plotkin91},
   488   pages		= {280-306}}
   489 
   490 @Article{dyckhoff,
   491   author	= {Roy Dyckhoff},
   492   title		= {Contraction-Free Sequent Calculi for Intuitionistic Logic},
   493   journal	= JSL,
   494   year		= 1992,
   495   volume	= 57,
   496   number	= 3,
   497   pages		= {795-807}}
   498 
   499 %F
   500 
   501 @Article{IMPS,
   502   author	= {William M. Farmer and Joshua D. Guttman and F. Javier
   503 		 Thayer},
   504   title		= {{IMPS}: An Interactive Mathematical Proof System},
   505   journal	= JAR,
   506   volume	= 11,
   507   number	= 2,
   508   year		= 1993,
   509   pages		= {213-248}}
   510 
   511 @InProceedings{felty91a,
   512   Author	= {Amy Felty},
   513   Title		= {A Logic Program for Transforming Sequent Proofs to Natural
   514 		  Deduction Proofs}, 
   515   crossref	= {extensions91},
   516   pages		= {157-178}}
   517 
   518 @Article{fleuriot-jcm,
   519   author = 	 {Jacques Fleuriot and Lawrence C. Paulson},
   520   title = 	 {Mechanizing Nonstandard Real Analysis},
   521   journal = 	 {LMS Journal of Computation and Mathematics},
   522   year = 	 2000,
   523   volume =	 3,
   524   pages =	 {140-190},
   525   note =	 {\url{http://www.lms.ac.uk/jcm/3/lms1999-027/}}
   526 }
   527 
   528 @TechReport{frost93,
   529   author	= {Jacob Frost},
   530   title		= {A Case Study of Co-induction in {Isabelle HOL}},
   531   institution	= CUCL,
   532   number	= 308,
   533   year		= 1993,
   534   month		= Aug}
   535 
   536 %revised version of frost93
   537 @TechReport{frost95,
   538   author	= {Jacob Frost},
   539   title		= {A Case Study of Co-induction in {Isabelle}},
   540   institution	= CUCL,
   541   number	= 359,
   542   year		= 1995,
   543   month		= Feb}
   544 
   545 @inproceedings{OBJ,
   546   author	= {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
   547 		 and J. Meseguer}, 
   548   title		= {Principles of {OBJ2}},
   549   booktitle	= POPL, 
   550   year		= 1985,
   551   pages		= {52-66}}
   552 
   553 %G
   554 
   555 @book{gallier86,
   556   author	= {J. H. Gallier},
   557   title		= {Logic for Computer Science: 
   558 		Foundations of Automatic Theorem Proving},
   559   year		= 1986,
   560   publisher	= {Harper \& Row}}
   561 
   562 @Book{galton90,
   563   author	= {Antony Galton},
   564   title		= {Logic for Information Technology},
   565   publisher	= {Wiley},
   566   year		= 1990}
   567 
   568 @Article{Gentzen:1935,
   569   author =       {G. Gentzen},
   570   title =        {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en},
   571   journal =      {Math. Zeitschrift},
   572   year =         1935
   573 }
   574 
   575 @InProceedings{gimenez-codifying,
   576   author	= {Eduardo Gim{\'e}nez},
   577   title		= {Codifying Guarded Definitions with Recursive Schemes},
   578   crossref	= {types94},
   579   pages		= {39-59}
   580 }
   581 
   582 @book{girard89,
   583   author	= {Jean-Yves Girard},
   584   title		= {Proofs and Types},
   585   year		= 1989,
   586   publisher	= CUP, 
   587   note		= {Translated by Yves LaFont and Paul Taylor}}
   588 
   589 @Book{mgordon-hol,
   590   editor	= {M. J. C. Gordon and T. F. Melham},
   591   title		= {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
   592   publisher	= CUP,
   593   year		= 1993}
   594 
   595 @book{mgordon79,
   596   author	= {Michael J. C. Gordon and Robin Milner and Christopher P.
   597 		 Wadsworth},
   598   title		= {Edinburgh {LCF}: A Mechanised Logic of Computation},
   599   year		= 1979,
   600   publisher	= {Springer},
   601   series	= {LNCS 78}}
   602 
   603 @inproceedings{Gunter-HOL92,author={Elsa L. Gunter},
   604 title={Why we can't have {SML} style datatype declarations in {HOL}},
   605 booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\
   606 IFIP TC10/WG10.2 Intl. Workshop, 1992},
   607 editor={L.J.M. Claesen and M.J.C. Gordon},
   608 publisher=NH,year=1993,pages={561--568}}
   609 
   610 @InProceedings{gunter-trees,
   611   author	= {Elsa L. Gunter},
   612   title		= {A Broader Class of Trees for Recursive Type Definitions for
   613 		  {HOL}},
   614   crossref	= {hug93},
   615   pages		= {141-154}}
   616 
   617 %H
   618 
   619 @InProceedings{Haftmann-Wenzel:2006:classes,
   620   author        = {Florian Haftmann and Makarius Wenzel},
   621   title         = {Constructive Type Classes in {Isabelle}},
   622   editor        = {T. Altenkirch and C. McBride},
   623   booktitle     = {Types for Proofs and Programs, TYPES 2006},
   624   publisher     = {Springer},
   625   series        = {LNCS},
   626   volume        = {4502},
   627   year          = {2007}
   628 }
   629 
   630 @inproceedings{Haftmann-Nipkow:2010:code,
   631   author =      {Florian Haftmann and Tobias Nipkow},
   632   title =       {Code Generation via Higher-Order Rewrite Systems},
   633   booktitle =   {Functional and Logic Programming: 10th International Symposium: FLOPS 2010},
   634   year =        2010,
   635   publisher =   Springer,
   636   series =      LNCS,
   637   editor =      {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
   638   volume =      6009
   639 }
   640 
   641 @InProceedings{Haftmann-Wenzel:2009,
   642   author        = {Florian Haftmann and Makarius Wenzel},
   643   title         = {Local theory specifications in {Isabelle/Isar}},
   644   editor        = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo},
   645   booktitle     = {Types for Proofs and Programs, TYPES 2008},
   646   publisher     = {Springer},
   647   series        = {LNCS},
   648   volume        = {5497},
   649   year          = {2009}
   650 }
   651 
   652 @inproceedings{hindleymilner,
   653   author = {L. Damas and H. Milner},
   654   title = {Principal type schemes for functional programs},
   655   booktitle = {ACM Symp. Principles of Programming Languages},
   656   year = 1982
   657 }
   658 
   659 @manual{isabelle-classes,
   660   author        = {Florian Haftmann},
   661   title         = {Haskell-style type classes with {Isabelle}/{Isar}},
   662   institution   = TUM,
   663   note          = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}
   664 }
   665 
   666 @manual{isabelle-codegen,
   667   author        = {Florian Haftmann},
   668   title         = {Code generation from Isabelle theories},
   669   institution   = TUM,
   670   note          = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}
   671 }
   672 
   673 @Book{halmos60,
   674   author	= {Paul R. Halmos},
   675   title		= {Naive Set Theory},
   676   publisher	= {Van Nostrand},
   677   year		= 1960}
   678 
   679 @book{HarelKT-DL,author={David Harel and Dexter Kozen and Jerzy Tiuryn},
   680 title={Dynamic Logic},publisher=MIT,year=2000}
   681 
   682 @Book{hennessy90,
   683   author	= {Matthew Hennessy},
   684   title		= {The Semantics of Programming Languages: An Elementary
   685 		  Introduction Using Structural Operational Semantics},
   686   publisher	= {Wiley},
   687   year		= 1990}
   688 
   689 @article{waldmeister,
   690   author = {Thomas Hillenbrand and Arnim Buch and Rolan Vogt and Bernd L\"ochner},
   691   title = "Waldmeister: High-Performance Equational Deduction",
   692   journal = JAR,
   693   volume	= 18,
   694   number	= 2,
   695   pages		= {265--270},
   696   year		= 1997}
   697 
   698 @book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman},
   699 title={Introduction to Automata Theory, Languages, and Computation.},
   700 publisher={Addison-Wesley},year=1979}
   701 
   702 @Article{haskell-report,
   703   author	= {Paul Hudak and Simon Peyton Jones and Philip Wadler},
   704   title		= {Report on the Programming Language {Haskell}: A
   705 		 Non-strict, Purely Functional Language},
   706   journal	= SIGPLAN,
   707   year		= 1992,
   708   volume	= 27,
   709   number	= 5,
   710   month		= May,
   711   note		= {Version 1.2}}
   712 
   713 @Article{haskell-tutorial,
   714   author	= {Paul Hudak and Joseph H. Fasel},
   715   title		= {A Gentle Introduction to {Haskell}},
   716   journal	= SIGPLAN,
   717   year		= 1992,
   718   volume	= 27,
   719   number	= 5,
   720   month		= May}
   721 
   722 @inproceedings{sine,
   723   author = "Kry\v{s}tof Hoder and Andrei Voronkov",
   724   title = "Sine Qua Non for Large Theory Reasoning",
   725   booktitle = {Automated Deduction --- CADE-23},
   726   publisher = Springer,
   727   series = LNCS,
   728   volume = 6803,
   729   pages = "299--314",
   730   editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
   731   year = 2011}
   732 
   733 @book{Hudak-Haskell,author={Paul Hudak},
   734 title={The Haskell School of Expression},publisher=CUP,year=2000}
   735 
   736 @article{huet75,
   737   author	= {G. P. Huet},
   738   title		= {A Unification Algorithm for Typed $\lambda$-Calculus},
   739   journal	= TCS,
   740   volume	= 1,
   741   year		= 1975,
   742   pages		= {27-57}}
   743 
   744 @article{huet78,
   745   author	= {G. P. Huet and B. Lang},
   746   title		= {Proving and Applying Program Transformations Expressed with 
   747 			Second-Order Patterns},
   748   journal	= acta,
   749   volume	= 11,
   750   year		= 1978, 
   751   pages		= {31-55}}
   752 
   753 @inproceedings{huet88,
   754   author	= {G{\'e}rard Huet},
   755   title		= {Induction Principles Formalized in the {Calculus of
   756 		 Constructions}}, 
   757   booktitle	= {Programming of Future Generation Computers},
   758   editor	= {K. Fuchi and M. Nivat},
   759   year		= 1988,
   760   pages		= {205-216}, 
   761   publisher	= {Elsevier}}
   762 
   763 @Book{Huth-Ryan-book,
   764   author	= {Michael Huth and Mark Ryan},
   765   title		= {Logic in Computer Science. Modelling and reasoning about systems},
   766   publisher	= CUP,
   767   year		= 2000}
   768 
   769 @InProceedings{Harrison:1996:MizarHOL,
   770   author = 	 {J. Harrison},
   771   title = 	 {A {Mizar} Mode for {HOL}},
   772   pages =	 {203--220},
   773   crossref =     {tphols96}}
   774 
   775 @misc{metis,
   776   author = "Joe Hurd",
   777   title = "Metis Theorem Prover",
   778   note = "\url{http://www.gilith.com/software/metis/}"}
   779 
   780 %J
   781 
   782 @article{haskell-revised-report,
   783   author =  {Simon {Peyton Jones} and others},
   784   title =   {The {Haskell} 98 Language and Libraries: The Revised Report},
   785   journal = {Journal of Functional Programming},
   786   volume =  13,
   787   number =  1,
   788   pages =   {0--255},
   789   month =   {Jan},
   790   year =    2003,
   791   note =    {\url{http://www.haskell.org/definition/}}}
   792 
   793 @book{jackson-2006,
   794   author = "Daniel Jackson",
   795   title = "Software Abstractions: Logic, Language, and Analysis",
   796   publisher = MIT,
   797   year = 2006}
   798 
   799 %K
   800 
   801 @InProceedings{kammueller-locales,
   802   author = 	 {Florian Kamm{\"u}ller and Markus Wenzel and 
   803                   Lawrence C. Paulson},
   804   title = 	 {Locales: A Sectioning Concept for {Isabelle}},
   805   crossref =	 {tphols99}}
   806 
   807 @book{Knuth3-75,
   808   author={Donald E. Knuth},
   809   title={The Art of Computer Programming, Volume 3: Sorting and Searching},
   810   publisher={Addison-Wesley},
   811   year=1975}
   812 
   813 @Article{korf85,
   814   author	= {R. E. Korf},
   815   title		= {Depth-First Iterative-Deepening: an Optimal Admissible
   816 		 Tree Search},
   817   journal	= AI,
   818   year		= 1985,
   819   volume	= 27,
   820   pages		= {97-109}}
   821 
   822 @inproceedings{korovin-2009,
   823   title = "Instantiation-Based Automated Reasoning: From Theory to Practice",
   824   author = "Konstantin Korovin",
   825   editor = "Renate A. Schmidt",
   826   booktitle = {Automated Deduction --- CADE-22},
   827   series = "LNAI",
   828   volume = {5663},
   829   pages = "163--166",
   830   year = 2009,
   831   publisher = "Springer"}
   832 
   833 @inproceedings{korovin-sticksel-2010,
   834   author    = {Konstantin Korovin and
   835                Christoph Sticksel},
   836   title     = {{iP}rover-{E}q: An Instantiation-Based Theorem Prover with Equality},
   837   pages     = {196--202},
   838   booktitle={Automated Reasoning: IJCAR 2010},
   839   editor={J. Giesl and R. H\"ahnle},
   840   publisher = Springer,
   841   series = LNCS,
   842   volume = 6173,
   843   year = 2010}
   844 
   845 @InProceedings{krauss2006,
   846   author   =  {Alexander Krauss},
   847   title    =  {Partial Recursive Functions in {Higher-Order Logic}},
   848   crossref =  {ijcar2006},
   849   pages =     {589--603}}
   850 
   851 @PhdThesis{krauss_phd,
   852 	author = {Alexander Krauss},
   853 	title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
   854   school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
   855 	year = {2009},
   856 	address = {Germany}
   857 }
   858 
   859 @manual{isabelle-function,
   860   author        = {Alexander Krauss},
   861   title         = {Defining Recursive Functions in {Isabelle/HOL}},
   862   institution   = TUM,
   863   note          = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
   864 }
   865 
   866 @Book{kunen80,
   867   author	= {Kenneth Kunen},
   868   title		= {Set Theory: An Introduction to Independence Proofs},
   869   publisher	= NH,
   870   year		= 1980}
   871 
   872 %L
   873 
   874 @manual{OCaml,
   875   author =  {Xavier Leroy and others},
   876   title =   {The Objective Caml system -- Documentation and user's manual},
   877   note =    {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}}
   878 
   879 @incollection{lochbihler-2010,
   880   title = "Coinduction",
   881   author = "Andreas Lochbihler",
   882   booktitle = "The Archive of Formal Proofs",
   883   editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
   884   publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
   885   month = "Feb.",
   886   year = 2010}
   887 
   888 @book{loveland-78,
   889   author = "D. W. Loveland",
   890   title = "Automated Theorem Proving: A Logical Basis",
   891   year = 1978,
   892   publisher = "North-Holland Publishing Co."}
   893 
   894 @InProceedings{lowe-fdr,
   895   author	= {Gavin Lowe},
   896   title		= {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
   897 		  Protocol using {CSP} and {FDR}},
   898   booktitle = 	 {Tools and Algorithms for the Construction and Analysis 
   899                   of Systems:  second international workshop, TACAS '96},
   900   editor =	 {T. Margaria and B. Steffen},
   901   series =	 {LNCS 1055},
   902   year =	 1996,
   903   publisher =	 {Springer},
   904   pages		= {147-166}}
   905 
   906 %M
   907 
   908 @Article{mw81,
   909   author	= {Zohar Manna and Richard Waldinger},
   910   title		= {Deductive Synthesis of the Unification Algorithm},
   911   journal	= SCP,
   912   year		= 1981,
   913   volume	= 1,
   914   number	= 1,
   915   pages		= {5-48}}
   916 
   917 @InProceedings{martin-nipkow,
   918   author	= {Ursula Martin and Tobias Nipkow},
   919   title		= {Ordered Rewriting and Confluence},
   920   crossref	= {cade10},
   921   pages		= {366-380}}
   922 
   923 @book{martinlof84,
   924   author	= {Per Martin-L{\"o}f},
   925   title		= {Intuitionistic type theory},
   926   year		= 1984,
   927   publisher	= {Bibliopolis}}
   928 
   929 @incollection{melham89,
   930   author	= {Thomas F. Melham},
   931   title		= {Automating Recursive Type Definitions in Higher Order
   932 		 Logic}, 
   933   pages		= {341-386},
   934   crossref	= {birtwistle89}}
   935 
   936 @Article{Miller:1991,
   937   author = 	 {Dale Miller},
   938   title = 	 {A Logic Programming Language with Lambda-Abstraction, Function Variables,
   939     and Simple Unification},
   940   journal = 	 {Journal of Logic and Computation},
   941   year = 	 1991,
   942   volume =	 1,
   943   number =	 4
   944 }
   945 
   946 @Article{miller-mixed,
   947   Author	= {Dale Miller},
   948   Title		= {Unification Under a Mixed Prefix},
   949   journal	= JSC,
   950   volume	= 14,
   951   number	= 4,
   952   pages		= {321-358},
   953   Year		= 1992}
   954 
   955 @Article{milner78,
   956   author	= {Robin Milner},
   957   title		= {A Theory of Type Polymorphism in Programming},
   958   journal	= "J. Comp.\ Sys.\ Sci.",
   959   year		= 1978,
   960   volume	= 17,
   961   pages		= {348-375}}
   962 
   963 @TechReport{milner-ind,
   964   author	= {Robin Milner},
   965   title		= {How to Derive Inductions in {LCF}},
   966   institution	= Edinburgh,
   967   year		= 1980,
   968   type		= {note}}
   969 
   970 @Article{milner-coind,
   971   author	= {Robin Milner and Mads Tofte},
   972   title		= {Co-induction in Relational Semantics},
   973   journal	= TCS,
   974   year		= 1991,
   975   volume	= 87,
   976   pages		= {209-220}}
   977 
   978 @Book{milner89,
   979   author	= {Robin Milner},
   980   title		= {Communication and Concurrency},
   981   publisher	= Prentice,
   982   year		= 1989}
   983 
   984 @book{SML,author="Robin Milner and Mads Tofte and Robert Harper",
   985 title="The Definition of Standard ML",publisher=MIT,year=1990}
   986 
   987 @PhdThesis{monahan84,
   988   author	= {Brian Q. Monahan},
   989   title		= {Data Type Proofs using Edinburgh {LCF}},
   990   school	= {University of Edinburgh},
   991   year		= 1984}
   992 
   993 @article{MuellerNvOS99,
   994 author=
   995 {Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
   996 title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191--223}}
   997 
   998 @Manual{Muzalewski:Mizar,
   999   title = 	 {An Outline of {PC} {Mizar}},
  1000   author =	 {Micha{\l} Muzalewski},
  1001   organization = {Fondation of Logic, Mathematics and Informatics
  1002                   --- Mizar Users Group},
  1003   year =	 1993,
  1004   note =	 {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}}
  1005 }
  1006 
  1007 %N
  1008 
  1009 @InProceedings{NaraschewskiW-TPHOLs98,
  1010   author	= {Wolfgang Naraschewski and Markus Wenzel},
  1011   title		= 
  1012 {Object-Oriented Verification based on Record Subtyping in
  1013                   Higher-Order Logic},
  1014   crossref      = {tphols98}}
  1015 
  1016 @inproceedings{nazareth-nipkow,
  1017   author	= {Dieter Nazareth and Tobias Nipkow},
  1018   title		= {Formal Verification of Algorithm {W}: The Monomorphic Case},
  1019   crossref	= {tphols96},
  1020   pages		= {331-345},
  1021   year		= 1996}
  1022 
  1023 @Article{needham-schroeder,
  1024   author =       "Roger M. Needham and Michael D. Schroeder",
  1025   title =        "Using Encryption for Authentication in Large Networks
  1026                  of Computers",
  1027   journal =      cacm,
  1028   volume =       21,
  1029   number =       12,
  1030   pages =        "993-999",
  1031   month =        dec,
  1032   year =         1978}
  1033 
  1034 @inproceedings{nipkow-W,
  1035   author	= {Wolfgang Naraschewski and Tobias Nipkow},
  1036   title		= {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
  1037   booktitle	= {Types for Proofs and Programs: Intl. Workshop TYPES '96},
  1038   editor	= {E. Gim{\'e}nez and C. Paulin-Mohring},
  1039   publisher	= Springer,
  1040   series	= LNCS,
  1041   volume	= 1512,
  1042   pages		= {317-332},
  1043   year		= 1998}
  1044 
  1045 @InCollection{nipkow-sorts93,
  1046   author = 	 {T. Nipkow},
  1047   title = 	 {Order-Sorted Polymorphism in {Isabelle}},
  1048   booktitle = 	 {Logical Environments},
  1049   publisher =	 CUP,
  1050   year =	 1993,
  1051   editor =	 {G. Huet and G. Plotkin},
  1052   pages =	 {164--188}
  1053 }
  1054 
  1055 @Misc{nipkow-types93,
  1056   author =	 {Tobias Nipkow},
  1057   title =	 {Axiomatic Type Classes (in {I}sabelle)},
  1058   howpublished = {Presentation at the workshop \emph{Types for Proof and Programs}, Nijmegen},
  1059   year =	 1993
  1060 }
  1061 
  1062 @inproceedings{Nipkow-CR,
  1063   author	= {Tobias Nipkow},
  1064   title		= {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
  1065   booktitle	= {Automated Deduction --- CADE-13},
  1066   editor	= {M. McRobbie and J.K. Slaney},
  1067   publisher	= Springer,
  1068   series	= LNCS,
  1069   volume	= 1104,
  1070   pages		= {733-747},
  1071   year		= 1996}
  1072 
  1073 % WAS Nipkow-LICS-93
  1074 @InProceedings{nipkow-patterns,
  1075   title		= {Functional Unification of Higher-Order Patterns},
  1076   author	= {Tobias Nipkow},
  1077   pages		= {64-74},
  1078   crossref	= {lics8},
  1079   url		= {\url{ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html}},
  1080   keywords	= {unification}}
  1081 
  1082 @article{nipkow-IMP,
  1083   author	= {Tobias Nipkow},
  1084   title		= {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
  1085   journal	= FAC,
  1086   volume	= 10,
  1087   pages		= {171-186},
  1088   year		= 1998}
  1089 
  1090 @inproceedings{Nipkow-TYPES02,
  1091   author        = {Tobias Nipkow},
  1092   title         = {{Structured Proofs in Isar/HOL}},
  1093   booktitle     = {Types for Proofs and Programs (TYPES 2002)},
  1094   editor        = {H. Geuvers and F. Wiedijk},
  1095   year          = 2003,
  1096   publisher     = Springer,
  1097   series        = LNCS,
  1098   volume        = 2646,
  1099   pages         = {259-278}}
  1100 
  1101 @manual{isabelle-HOL,
  1102   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  1103   title		= {{Isabelle}'s Logics: {HOL}},
  1104   institution	= {Institut f{\"u}r Informatik, Technische Universi{\"a}t
  1105                   M{\"u}nchen and Computer Laboratory, University of Cambridge},
  1106   note          = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
  1107 
  1108 @article{nipkow-prehofer,
  1109   author	= {Tobias Nipkow and Christian Prehofer},
  1110   title		= {Type Reconstruction for Type Classes},
  1111   journal	= JFP,
  1112   volume	= 5,
  1113   number	= 2,
  1114   year		= 1995,
  1115   pages		= {201-224}}
  1116 
  1117 @InProceedings{Nipkow-Prehofer:1993,
  1118   author =       {T. Nipkow and C. Prehofer},
  1119   title =        {Type checking type classes},
  1120   booktitle =    {ACM Symp.\ Principles of Programming Languages},
  1121   year =         1993
  1122 }
  1123 
  1124 @Book{isa-tutorial,
  1125   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  1126   title		= {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic},
  1127   publisher	= Springer,
  1128   year		= 2002,
  1129   series    = LNCS,
  1130   volume    = 2283}
  1131 
  1132 @Article{noel,
  1133   author	= {Philippe No{\"e}l},
  1134   title		= {Experimenting with {Isabelle} in {ZF} Set Theory},
  1135   journal	= JAR,
  1136   volume	= 10,
  1137   number	= 1,
  1138   pages		= {15-58},
  1139   year		= 1993}
  1140 
  1141 @book{nordstrom90,
  1142   author	= {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith},
  1143   title		= {Programming in {Martin-L{\"o}f}'s Type Theory.  An
  1144 		 Introduction}, 
  1145   publisher	= {Oxford University Press}, 
  1146   year		= 1990}
  1147 
  1148 %O
  1149 
  1150 @TechReport{scala-overview-tech-report,
  1151   author =       {Martin Odersky and al.},
  1152   title =        {An Overview of the Scala Programming Language},
  1153   institution =  {EPFL Lausanne, Switzerland},
  1154   year =         2004,
  1155   number =       {IC/2004/64}
  1156 }
  1157 
  1158 @Article{Oppen:1980,
  1159   author =       {D. C. Oppen},
  1160   title =        {Pretty Printing},
  1161   journal =      {ACM Transactions on Programming Languages and Systems},
  1162   year =         1980,
  1163   volume =    2,
  1164   number =    4}
  1165 
  1166 @Manual{pvs-language,
  1167   title		= {The {PVS} specification language},
  1168   author	= {S. Owre and N. Shankar and J. M. Rushby},
  1169   organization	= {Computer Science Laboratory, SRI International},
  1170   address	= {Menlo Park, CA},
  1171   note          = {Beta release},
  1172   year		= 1993,
  1173   month		= apr,
  1174   url		= {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}}
  1175 
  1176 %P
  1177 
  1178 % replaces paulin92
  1179 @InProceedings{paulin-tlca,
  1180   author	= {Christine Paulin-Mohring},
  1181   title		= {Inductive Definitions in the System {Coq}: Rules and
  1182 		 Properties},
  1183   crossref	= {tlca93},
  1184   pages		= {328-345}}
  1185 
  1186 @InProceedings{paulson-CADE,
  1187   author	= {Lawrence C. Paulson},
  1188   title		= {A Fixedpoint Approach to Implementing (Co)Inductive
  1189 		  Definitions},
  1190   pages		= {148-161},
  1191   crossref	= {cade12}}
  1192 
  1193 @InProceedings{paulson-COLOG,
  1194   author	= {Lawrence C. Paulson},
  1195   title		= {A Formulation of the Simple Theory of Types (for
  1196 		 {Isabelle})}, 
  1197   pages		= {246-274},
  1198   crossref	= {colog88},
  1199   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}
  1200 
  1201 @Article{paulson-coind,
  1202   author	= {Lawrence C. Paulson},
  1203   title		= {Mechanizing Coinduction and Corecursion in Higher-Order
  1204 		  Logic},
  1205   journal	= JLC,
  1206   year		= 1997,
  1207   volume	= 7,
  1208   number	= 2,
  1209   month		= mar,
  1210   pages		= {175-204}}
  1211 
  1212 @manual{isabelle-intro,
  1213   author	= {Lawrence C. Paulson},
  1214   title		= {Old Introduction to {Isabelle}},
  1215   institution	= CUCL,
  1216   note          = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}}
  1217 
  1218 @manual{isabelle-logics,
  1219   author	= {Lawrence C. Paulson},
  1220   title		= {{Isabelle's} Logics},
  1221   institution	= CUCL,
  1222   note          = {\url{http://isabelle.in.tum.de/doc/logics.pdf}}}
  1223 
  1224 @manual{isabelle-ref,
  1225   author	= {Lawrence C. Paulson},
  1226   title		= {The Old {Isabelle} Reference Manual},
  1227   institution	= CUCL,
  1228   note          = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}}
  1229 
  1230 @manual{isabelle-ZF,
  1231   author	= {Lawrence C. Paulson},
  1232   title		= {{Isabelle}'s Logics: {FOL} and {ZF}},
  1233   institution	= CUCL,
  1234   note          = {\url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}}}
  1235 
  1236 @article{paulson-found,
  1237   author	= {Lawrence C. Paulson},
  1238   title		= {The Foundation of a Generic Theorem Prover},
  1239   journal	= JAR,
  1240   volume	= 5,
  1241   number	= 3,
  1242   pages		= {363-397},
  1243   year		= 1989,
  1244   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}}
  1245 
  1246 %replaces paulson-final
  1247 @Article{paulson-mscs,
  1248   author	= {Lawrence C. Paulson},
  1249   title = 	 {Final Coalgebras as Greatest Fixed Points 
  1250                   in {ZF} Set Theory},
  1251   journal	= {Mathematical Structures in Computer Science},
  1252   year		= 1999,
  1253   volume	= 9,
  1254   number = 5,
  1255   pages = {545-567}}
  1256 
  1257 @InCollection{paulson-generic,
  1258   author	= {Lawrence C. Paulson},
  1259   title		= {Generic Automatic Proof Tools},
  1260   crossref	= {wos-fest},
  1261   chapter	= 3}
  1262 
  1263 @Article{paulson-gr,
  1264   author	= {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
  1265   title		= {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of
  1266 		  Choice},
  1267   journal	= JAR,
  1268   year		= 1996,
  1269   volume	= 17,
  1270   number	= 3,
  1271   month		= dec,
  1272   pages		= {291-323}}
  1273 
  1274 @InCollection{paulson-fixedpt-milner,
  1275   author	= {Lawrence C. Paulson},
  1276   title		= {A Fixedpoint Approach to (Co)inductive and
  1277                   (Co)datatype Definitions},
  1278   pages		= {187-211},
  1279   crossref	= {milner-fest}}
  1280 
  1281 @book{milner-fest,
  1282   title		= {Proof, Language, and Interaction: 
  1283                    Essays in Honor of {Robin Milner}},
  1284   booktitle	= {Proof, Language, and Interaction: 
  1285                    Essays in Honor of {Robin Milner}},
  1286   publisher	= MIT,
  1287   year		= 2000,
  1288   editor	= {Gordon Plotkin and Colin Stirling and Mads Tofte}}
  1289 
  1290 @InCollection{paulson-handbook,
  1291   author	= {Lawrence C. Paulson},
  1292   title		= {Designing a Theorem Prover},
  1293   crossref	= {handbk-lics2},
  1294   pages		= {415-475}}
  1295 
  1296 @Book{paulson-isa-book,
  1297   author	= {Lawrence C. Paulson},
  1298   title		= {Isabelle: A Generic Theorem Prover},
  1299   publisher	= {Springer},
  1300   year		= 1994,
  1301   note		= {LNCS 828}}
  1302 
  1303 @Book{isabelle-hol-book,
  1304   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  1305   title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  1306   publisher	= {Springer},
  1307   year		= 2002,
  1308   note		= {LNCS 2283}}
  1309 
  1310 @InCollection{paulson-markt,
  1311   author	= {Lawrence C. Paulson},
  1312   title		= {Tool Support for Logics of Programs},
  1313   booktitle	= {Mathematical Methods in Program Development:
  1314                   Summer School Marktoberdorf 1996},
  1315   publisher	= {Springer},
  1316   pages		= {461-498},
  1317   year		= {Published 1997},
  1318   editor	= {Manfred Broy},
  1319   series	= {NATO ASI Series F}}
  1320 
  1321 %replaces Paulson-ML and paulson91
  1322 @book{paulson-ml2,
  1323   author	= {Lawrence C. Paulson},
  1324   title		= {{ML} for the Working Programmer},
  1325   year		= 1996,
  1326   edition	= {2nd},
  1327   publisher	= CUP}
  1328 
  1329 @article{paulson-natural,
  1330   author	= {Lawrence C. Paulson},
  1331   title		= {Natural Deduction as Higher-order Resolution},
  1332   journal	= JLP,
  1333   volume	= 3,
  1334   pages		= {237-258},
  1335   year		= 1986,
  1336   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}}
  1337 
  1338 @Article{paulson-set-I,
  1339   author	= {Lawrence C. Paulson},
  1340   title		= {Set Theory for Verification: {I}.  {From}
  1341 		 Foundations to Functions},
  1342   journal	= JAR,
  1343   volume	= 11,
  1344   number	= 3,
  1345   pages		= {353-389},
  1346   year		= 1993,
  1347   url		= {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/set-I.pdf}}}
  1348 
  1349 @Article{paulson-set-II,
  1350   author	= {Lawrence C. Paulson},
  1351   title		= {Set Theory for Verification: {II}.  {Induction} and
  1352 		 Recursion},
  1353   journal	= JAR,
  1354   volume	= 15,
  1355   number	= 2,
  1356   pages		= {167-215},
  1357   year		= 1995,
  1358   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}}
  1359 
  1360 @article{paulson85,
  1361   author	= {Lawrence C. Paulson},
  1362   title		= {Verifying the Unification Algorithm in {LCF}},
  1363   journal	= SCP,
  1364   volume	= 5,
  1365   pages		= {143-170},
  1366   year		= 1985}
  1367 
  1368 %replaces Paulson-LCF
  1369 @book{paulson87,
  1370   author	= {Lawrence C. Paulson},
  1371   title		= {Logic and Computation: Interactive proof with Cambridge
  1372 		 LCF}, 
  1373   year		= 1987,
  1374   publisher	= CUP}
  1375 
  1376 @incollection{paulson700,
  1377   author	= {Lawrence C. Paulson},
  1378   title		= {{Isabelle}: The Next 700 Theorem Provers},
  1379   crossref	= {odifreddi90},
  1380   pages		= {361-386},
  1381   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}}
  1382 
  1383 % replaces paulson-ns and paulson-security
  1384 @Article{paulson-jcs,
  1385   author	= {Lawrence C. Paulson},
  1386   title		= {The Inductive Approach to Verifying Cryptographic Protocols},
  1387   journal	= JCS,
  1388   year		= 1998,
  1389   volume	= 6,
  1390   pages		= {85-128}}
  1391 
  1392 @Article{paulson-tls,
  1393   author = 	 {Lawrence C. Paulson},
  1394   title = 	 {Inductive Analysis of the {Internet} Protocol {TLS}},
  1395   journal = 	 TISSEC,
  1396   month =        aug,
  1397   year = 	 1999,
  1398   volume	= 2,
  1399   number        = 3,
  1400   pages		= {332-351}}
  1401 
  1402 @Article{paulson-yahalom,
  1403   author = 	 {Lawrence C. Paulson},
  1404   title = 	 {Relations Between Secrets:
  1405                   Two Formal Analyses of the {Yahalom} Protocol},
  1406   journal = 	 JCS,
  1407   volume = 9,
  1408   number = 3,
  1409   pages = {197-216},
  1410   year = 2001}}
  1411 
  1412 @article{pelletier86,
  1413   author	= {F. J. Pelletier},
  1414   title		= {Seventy-five Problems for Testing Automatic Theorem
  1415 		 Provers}, 
  1416   journal	= JAR,
  1417   volume	= 2,
  1418   pages		= {191-216},
  1419   year		= 1986,
  1420   note		= {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}
  1421 
  1422 @InCollection{pitts93,
  1423   author =       {A. Pitts},
  1424   title =        {The {HOL} Logic},
  1425   editor =       {M. J. C. Gordon and T. F. Melham},
  1426   booktitle  =   {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
  1427   pages =        {191--232},
  1428   publisher	= CUP,
  1429   year		= 1993}
  1430 
  1431 @Article{pitts94,  
  1432   author	= {Andrew M. Pitts},
  1433   title		= {A Co-induction Principle for Recursively Defined Domains},
  1434   journal	= TCS,
  1435   volume	= 124, 
  1436   pages		= {195-219},
  1437   year		= 1994} 
  1438 
  1439 @Article{plaisted90,
  1440   author	= {David A. Plaisted},
  1441   title		= {A Sequent-Style Model Elimination Strategy and a Positive
  1442 		 Refinement},
  1443   journal	= JAR,
  1444   year		= 1990,
  1445   volume	= 6,
  1446   number	= 4,
  1447   pages		= {389-402}}
  1448 
  1449 %Q
  1450 
  1451 @Article{quaife92,
  1452   author	= {Art Quaife},
  1453   title		= {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set
  1454 		 Theory},
  1455   journal	= JAR,
  1456   year		= 1992,
  1457   volume	= 8,
  1458   number	= 1,
  1459   pages		= {91-147}}
  1460 
  1461 %R
  1462 
  1463 @TechReport{rasmussen95,
  1464   author	= {Ole Rasmussen},
  1465   title		= {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
  1466 		  Experiment},
  1467   institution	= {Computer Laboratory, University of Cambridge},
  1468   year		= 1995,
  1469   number	= 364,
  1470   month		= may,
  1471   url		= {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}}
  1472 
  1473 @Book{reeves90,
  1474   author	= {Steve Reeves and Michael Clarke},
  1475   title		= {Logic for Computer Science},
  1476   publisher	= {Addison-Wesley},
  1477   year		= 1990}
  1478 
  1479 @article{riazanov-voronkov-2002,
  1480   author = "Alexander Riazanov and Andrei Voronkov",
  1481   title = "The Design and Implementation of {Vampire}",
  1482   journal = "Journal of AI Communications",
  1483   year = 2002,
  1484   volume = 15,
  1485   number ="2/3",
  1486   pages = "91--110"}
  1487 
  1488 @book{Rosen-DMA,author={Kenneth H. Rosen},
  1489 title={Discrete Mathematics and Its Applications},
  1490 publisher={McGraw-Hill},year=1998}
  1491 
  1492 @InProceedings{Rudnicki:1992:MizarOverview,
  1493   author = 	 {P. Rudnicki},
  1494   title = 	 {An Overview of the {MIZAR} Project},
  1495   booktitle = 	 {1992 Workshop on Types for Proofs and Programs},
  1496   year =	 1992,
  1497   organization = {Chalmers University of Technology},
  1498   publisher =	 {Bastad}
  1499 }
  1500 
  1501 %S
  1502 
  1503 @inproceedings{saaltink-fme,
  1504   author	= {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
  1505 		 Dan Craigen and Irwin Meisels},
  1506   title		= {An {EVES} Data Abstraction Example}, 
  1507   pages		= {578-596},
  1508   crossref	= {fme93}}
  1509 
  1510 @Article{Schroeder-Heister:1984,
  1511   author =       {Peter Schroeder-Heister},
  1512   title =        {A Natural Extension of Natural Deduction},
  1513   journal =      {Journal of Symbolic Logic},
  1514   year =         1984,
  1515   volume =       49,
  1516   number =       4
  1517 }
  1518 
  1519 @article{schulz-2002,
  1520   author = "Stephan Schulz",
  1521   title = "E---A Brainiac Theorem Prover",
  1522   journal = "Journal of AI Communications",
  1523   year = 2002,
  1524   volume = 15,
  1525   number ="2/3",
  1526   pages = "111--126"}
  1527 
  1528 @misc{sledgehammer-2009,
  1529   key = "Sledgehammer",
  1530   title = "The {S}ledgehammer: Let Automatic Theorem Provers
  1531 Write Your {I}s\-a\-belle Scripts",
  1532   note = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/sledgehammer.html}"}
  1533 
  1534 @inproceedings{slind-tfl,
  1535   author	= {Konrad Slind},
  1536   title		= {Function Definition in Higher Order Logic},
  1537   crossref  = {tphols96},
  1538   pages		= {381-397}}
  1539 
  1540 @inproceedings{snark,
  1541   author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood},
  1542   title = {Deductive composition of astronomical software from subroutine libraries},
  1543   pages = "341--355",
  1544   crossref = {cade12}}
  1545 
  1546 @book{suppes72,
  1547   author	= {Patrick Suppes},
  1548   title		= {Axiomatic Set Theory},
  1549   year		= 1972,
  1550   publisher	= {Dover}}
  1551 
  1552 @inproceedings{sutcliffe-2000,
  1553   author = "Geoff Sutcliffe",
  1554   title = "System Description: {SystemOnTPTP}",
  1555   editor = "David McAllester",
  1556   booktitle	= {Automated Deduction --- {CADE}-17 International Conference},
  1557   series = "Lecture Notes in Artificial Intelligence",
  1558   volume = {1831},
  1559   pages = "406--410",
  1560   year = 2000,
  1561   publisher = Springer}
  1562 
  1563 @misc{tofof,
  1564   author = "Geoff Sutcliffe",
  1565   title = "{ToFoF}",
  1566   note = "\url{http://www.cs.miami.edu/~tptp/ATPSystems/ToFoF/}"}
  1567 
  1568 @Article{Sutter:2005,
  1569   author = 	 {H. Sutter},
  1570   title = 	 {The Free Lunch Is Over --- A Fundamental Turn Toward Concurrency in Software},
  1571   journal = 	 {Dr. Dobb's Journal},
  1572   year = 	 2005,
  1573   volume = 	 30,
  1574   number = 	 3}
  1575 
  1576 @InCollection{szasz93,
  1577   author	= {Nora Szasz},
  1578   title		= {A Machine Checked Proof that {Ackermann's} Function is not
  1579 		  Primitive Recursive},
  1580   crossref	= {huet-plotkin93},
  1581   pages		= {317-338}}
  1582 
  1583 @TechReport{Syme:1997:DECLARE,
  1584   author = 	 {D. Syme},
  1585   title = 	 {{DECLARE}: A Prototype Declarative Proof System for Higher Order Logic},
  1586   institution =  {University of Cambridge Computer Laboratory},
  1587   year = 	 1997,
  1588   number =	 416
  1589 }
  1590 
  1591 @PhdThesis{Syme:1998:thesis,
  1592   author = 	 {D. Syme},
  1593   title = 	 {Declarative Theorem Proving for Operational Semantics},
  1594   school = 	 {University of Cambridge},
  1595   year = 	 1998,
  1596   note =	 {Submitted}
  1597 }
  1598 
  1599 @InProceedings{Syme:1999:TPHOL,
  1600   author = 	 {D. Syme},
  1601   title = 	 {Three Tactic Theorem Proving},
  1602   crossref =     {tphols99}}
  1603 
  1604 %T
  1605 
  1606 @book{takeuti87,
  1607   author	= {G. Takeuti},
  1608   title		= {Proof Theory},
  1609   year		= 1987,
  1610   publisher	= NH,
  1611   edition	= {2nd}}
  1612 
  1613 @Book{thompson91,
  1614   author	= {Simon Thompson},
  1615   title		= {Type Theory and Functional Programming},
  1616   publisher	= {Addison-Wesley},
  1617   year		= 1991}
  1618 
  1619 @book{Thompson-Haskell,author={Simon Thompson},
  1620 title={Haskell: The Craft of Functional Programming},
  1621 publisher={Addison-Wesley},year=1999}
  1622 
  1623 @misc{kodkod-2009,
  1624   author = "Emina Torlak",
  1625   title = {Kodkod: Constraint Solver for Relational Logic},
  1626   note = "\url{http://alloy.mit.edu/kodkod/}"}
  1627 
  1628 @misc{kodkod-2009-options,
  1629   author = "Emina Torlak",
  1630   title = "Kodkod {API}: Class {Options}",
  1631   note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"}
  1632 
  1633 @inproceedings{torlak-jackson-2007,
  1634   title = "Kodkod: A Relational Model Finder",
  1635   author = "Emina Torlak and Daniel Jackson",
  1636   editor = "Orna Grumberg and Michael Huth",
  1637   booktitle = "TACAS 2007",
  1638   series = LNCS,
  1639   volume = {4424},
  1640   pages = "632--647",
  1641   year = 2007,
  1642   publisher = Springer}
  1643 
  1644 @unpublished{traytel-berghofer-nipkow-2011,
  1645   author = {D. Traytel and S. Berghofer and T. Nipkow},
  1646   title = {Extending Hindley-Milner Type Inference with Coercive
  1647       Subtyping (long version)},
  1648   year = 2011,
  1649   note = {Submitted,
  1650       \url{http://isabelle.in.tum.de/doc/implementation.pdf}}},
  1651 }
  1652 
  1653 @Unpublished{Trybulec:1993:MizarFeatures,
  1654   author = 	 {A. Trybulec},
  1655   title = 	 {Some Features of the {Mizar} Language},
  1656   note = 	 {Presented at a workshop in Turin, Italy},
  1657   year =	 1993
  1658 }
  1659 
  1660 %V
  1661 
  1662 @Unpublished{voelker94,
  1663   author	= {Norbert V{\"o}lker},
  1664   title		= {The Verification of a Timer Program using {Isabelle/HOL}},
  1665   url		= {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}},
  1666   year		= 1994,
  1667   month		= aug}
  1668 
  1669 %W
  1670 
  1671 @inproceedings{wadler89how,
  1672   author        = {P. Wadler and S. Blott},
  1673   title         = {How to make ad-hoc polymorphism less ad-hoc},
  1674   booktitle     = {ACM Symp.\ Principles of Programming Languages},
  1675   year          = 1989
  1676 }
  1677 
  1678 @phdthesis{weber-2008,
  1679   author = "Tjark Weber",
  1680   title = "SAT-Based Finite Model Generation for Higher-Order Logic",
  1681   school = {Dept.\ of Informatics, T.U. M\"unchen},
  1682   type = "{Ph.D.}\ thesis",
  1683   year = 2008}
  1684 
  1685 @Misc{x-symbol,
  1686   author =	 {Christoph Wedler},
  1687   title =	 {Emacs package ``{X-Symbol}''},
  1688   note =	 {\url{http://x-symbol.sourceforge.net}}
  1689 }
  1690 
  1691 @misc{weidenbach-et-al-2009,
  1692   author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski",
  1693   title = "{SPASS} Version 3.5",
  1694   note = {\url{http://www.spass-prover.org/publications/spass.pdf}}}
  1695 
  1696 @manual{isabelle-sys,
  1697   author	= {Markus Wenzel and Stefan Berghofer},
  1698   title		= {The {Isabelle} System Manual},
  1699   institution	= {TU Munich},
  1700   note          = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}
  1701 
  1702 @manual{isabelle-isar-ref,
  1703   author	= {Makarius Wenzel},
  1704   title		= {The {Isabelle/Isar} Reference Manual},
  1705   institution	= {TU Munich},
  1706   note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
  1707 
  1708 @manual{isabelle-implementation,
  1709   author	= {Makarius Wenzel},
  1710   title		= {The {Isabelle/Isar} Implementation},
  1711   institution	= {TU Munich},
  1712   note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
  1713 
  1714 @InProceedings{Wenzel:1999:TPHOL,
  1715   author = 	 {Markus Wenzel},
  1716   title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
  1717   crossref =     {tphols99}}
  1718 
  1719 @InProceedings{Wenzel:1997:TPHOL,
  1720   author = 	 {Markus Wenzel},
  1721   title = 	 {Type Classes and Overloading in Higher-Order Logic},
  1722   crossref =     {tphols97}}
  1723 
  1724 @phdthesis{Wenzel-PhD,
  1725   author={Markus Wenzel},
  1726     title={Isabelle/Isar --- a versatile environment for human-readable formal proof documents},
  1727   school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
  1728   year=2002,
  1729   note =	 {\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}}}
  1730 
  1731 @Article{Wenzel-Wiedijk:2002,
  1732   author = 	 {Freek Wiedijk and Markus Wenzel},
  1733   title = 	 {A comparison of the mathematical proof languages {Mizar} and {Isar}.},
  1734   journal = 	 {Journal of Automated Reasoning},
  1735   year = 	 2002,
  1736   volume =	 29,
  1737   number =	 {3-4}
  1738 }
  1739 
  1740 @InCollection{Wenzel-Paulson:2006,
  1741   author = 	 {Markus Wenzel and Lawrence C. Paulson},
  1742   title = 	 {{Isabelle/Isar}},
  1743   booktitle = 	 {The Seventeen Provers of the World},
  1744   year =	 2006,
  1745   editor =	 {F. Wiedijk},
  1746   series =	 {LNAI 3600}
  1747 }
  1748 
  1749 @InCollection{Wenzel:2006:Festschrift,
  1750   author = 	 {Makarius Wenzel},
  1751   title = 	 {{Isabelle/Isar} --- a generic framework for human-readable proof documents},
  1752   booktitle = 	 {From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec},
  1753   publisher =	 {University of Bia{\l}ystok},
  1754   year =	 2007,
  1755   editor =	 {R. Matuszewski and A. Zalewska},
  1756   volume =	 {10(23)},
  1757   series =	 {Studies in Logic, Grammar, and Rhetoric},
  1758   note =         {\url{http://www.in.tum.de/~wenzelm/papers/isar-framework.pdf}}
  1759 }
  1760 
  1761 @InProceedings{Wenzel-Chaieb:2007b,
  1762   author = {Makarius Wenzel and Amine Chaieb},
  1763   title = {{SML} with antiquotations embedded into {Isabelle/Isar}},
  1764   booktitle = {Workshop on Programming Languages for Mechanized Mathematics
  1765     (satellite of CALCULEMUS 2007). Hagenberg, Austria},
  1766   editor = {Jacques Carette and Freek Wiedijk},
  1767   month = {June},
  1768   year = {2007}
  1769 }
  1770 
  1771 @InProceedings{Wenzel:2009,
  1772   author = 	 {M. Wenzel},
  1773   title = 	 {Parallel Proof Checking in {Isabelle/Isar}},
  1774   booktitle = {ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009)},
  1775   year = 	 2009,
  1776   editor = 	 {Dos Reis, G. and L. Th\'ery},
  1777   publisher = {ACM Digital Library}}
  1778 
  1779 @book{principia,
  1780   author	= {A. N. Whitehead and B. Russell},
  1781   title		= {Principia Mathematica},
  1782   year		= 1962,
  1783   publisher	= CUP, 
  1784   note		= {Paperback edition to *56,
  1785   abridged from the 2nd edition (1927)}}
  1786 
  1787 @Misc{Wiedijk:1999:Mizar,
  1788   author =	 {Freek Wiedijk},
  1789   title =	 {Mizar: An Impression},
  1790   howpublished = {Unpublished paper},
  1791   year =         1999,
  1792   note =	 {\url{http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz}}
  1793 }
  1794 
  1795 @Misc{Wiedijk:2000:MV,
  1796   author =	 {Freek Wiedijk},
  1797   title =	 {The Mathematical Vernacular},
  1798   howpublished = {Unpublished paper},
  1799   year =         2000,
  1800   note =	 {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}}
  1801 }
  1802 
  1803 @misc{wikipedia-2009-aa-trees,
  1804   key = "Wikipedia",
  1805   title = "Wikipedia: {AA} Tree",
  1806   note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
  1807 
  1808 @book{winskel93,
  1809   author	= {Glynn Winskel},
  1810   title		= {The Formal Semantics of Programming Languages},
  1811   publisher	= MIT,year=1993}
  1812 
  1813 @InCollection{wos-bledsoe,
  1814   author	= {Larry Wos},
  1815   title		= {Automated Reasoning and {Bledsoe's} Dream for the Field},
  1816   crossref	= {bledsoe-fest},
  1817   pages		= {297-342}}
  1818 
  1819 @InProceedings{Zammit:1999:TPHOL,
  1820   author = 	 {Vincent Zammit},
  1821   title = 	 {On the Implementation of an Extensible Declarative Proof Language},
  1822   crossref =     {tphols99}}
  1823 
  1824 %Z
  1825 
  1826 @misc{z3,
  1827   key = "Z3",
  1828   title = "Z3: An Efficient {SMT} Solver",
  1829   note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"}
  1830 
  1831 
  1832 % CROSS REFERENCES
  1833 
  1834 @book{handbk-lics2,
  1835   editor	= {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
  1836   title		= {Handbook of Logic in Computer Science},
  1837   booktitle	= {Handbook of Logic in Computer Science},
  1838   publisher	= {Oxford University Press},
  1839   year		= 1992,
  1840   volume	= 2}
  1841 
  1842 @book{types93,
  1843   editor	= {Henk Barendregt and Tobias Nipkow},
  1844   title		= TYPES # {: International Workshop {TYPES '93}},
  1845   booktitle	= TYPES # {: International Workshop {TYPES '93}},
  1846   year		= {published 1994},
  1847   publisher	= {Springer},
  1848   series	= {LNCS 806}}
  1849 
  1850 @book{barwise-handbk,
  1851   editor	= {J. Barwise},
  1852   title		= {Handbook of Mathematical Logic},
  1853   booktitle	= {Handbook of Mathematical Logic},
  1854   year		= 1977,
  1855   publisher	= NH}
  1856 
  1857 @Proceedings{tlca93,
  1858   title		= {Typed Lambda Calculi and Applications},
  1859   booktitle	= {Typed Lambda Calculi and Applications},
  1860   editor	= {M. Bezem and J.F. Groote},
  1861   year		= 1993,
  1862   publisher	= {Springer},
  1863   series	= {LNCS 664}}
  1864 
  1865 @book{birtwistle89,
  1866   editor	= {Graham Birtwistle and P. A. Subrahmanyam},
  1867   title		= {Current Trends in Hardware Verification and Automated
  1868 		 Theorem Proving}, 
  1869   booktitle	= {Current Trends in Hardware Verification and Automated
  1870 		 Theorem Proving}, 
  1871   publisher	= {Springer},
  1872   year		= 1989}
  1873 
  1874 @book{bledsoe-fest,
  1875   title		= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
  1876   booktitle	= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
  1877   publisher	= {Kluwer Academic Publishers},
  1878   year		= 1991,
  1879   editor	= {Robert S. Boyer}}
  1880 
  1881 @Proceedings{cade12,
  1882   editor	= {Alan Bundy},
  1883   title		= {Automated Deduction --- {CADE}-12 
  1884 		  International Conference},
  1885   booktitle	= {Automated Deduction --- {CADE}-12 
  1886 		  International Conference},
  1887   year		= 1994,
  1888   series	= {LNAI 814},
  1889   publisher	= {Springer}}
  1890 
  1891 @book{types94,
  1892   editor	= {Peter Dybjer and Bengt Nordstr{{\"o}m} and Jan Smith},
  1893   title		= TYPES # {: International Workshop {TYPES '94}},
  1894   booktitle	= TYPES # {: International Workshop {TYPES '94}},
  1895   year		= 1995,
  1896   publisher	= {Springer},
  1897   series	= {LNCS 996}}
  1898 
  1899 @book{huet-plotkin91,
  1900   editor	= {{G{\'e}rard} Huet and Gordon Plotkin},
  1901   title		= {Logical Frameworks},
  1902   booktitle	= {Logical Frameworks},
  1903   publisher	= CUP,
  1904   year		= 1991}
  1905 
  1906 @book{huet-plotkin93,
  1907   editor	= {{G{\'e}rard} Huet and Gordon Plotkin},
  1908   title		= {Logical Environments},
  1909   booktitle	= {Logical Environments},
  1910   publisher	= CUP,
  1911   year		= 1993}
  1912 
  1913 @Proceedings{hug93,
  1914   editor	= {J. Joyce and C. Seger},
  1915   title		= {Higher Order Logic Theorem Proving and Its
  1916 		  Applications: HUG '93},
  1917   booktitle	= {Higher Order Logic Theorem Proving and Its
  1918 		  Applications: HUG '93},
  1919   year		= {Published 1994},
  1920   publisher	= {Springer},
  1921   series	= {LNCS 780}}
  1922 
  1923 @proceedings{colog88,
  1924   editor	= {P. Martin-L{\"o}f and G. Mints},
  1925   title		= {COLOG-88: International Conference on Computer Logic},
  1926   booktitle	= {COLOG-88: International Conference on Computer Logic},
  1927   year		= {Published 1990},
  1928   publisher	= {Springer},
  1929   organization	= {Estonian Academy of Sciences},
  1930   address	= {Tallinn},
  1931   series	= {LNCS 417}}
  1932 
  1933 @book{odifreddi90,
  1934   editor	= {P. Odifreddi},
  1935   title		= {Logic and Computer Science},
  1936   booktitle	= {Logic and Computer Science},
  1937   publisher	= {Academic Press},
  1938   year		= 1990}
  1939 
  1940 @proceedings{extensions91,
  1941   editor	= {Peter Schroeder-Heister},
  1942   title		= {Extensions of Logic Programming},
  1943   booktitle	= {Extensions of Logic Programming},
  1944   year		= 1991,
  1945   series	= {LNAI 475}, 
  1946   publisher	= {Springer}}
  1947 
  1948 @proceedings{cade10,
  1949   editor	= {Mark E. Stickel},
  1950   title		= {10th } # CADE,
  1951   booktitle	= {10th } # CADE,
  1952   year		= 1990,
  1953   publisher	= {Springer},
  1954   series	= {LNAI 449}}
  1955 
  1956 @Proceedings{lics8,
  1957   editor	= {M. Vardi},
  1958   title		= {Eighth Annual Symposium on Logic in Computer Science},
  1959   booktitle	= {Eighth Annual Symposium on Logic in Computer Science},
  1960   publisher	= IEEE,
  1961   year		= 1993}
  1962 
  1963 @book{wos-fest,
  1964   title		= {Automated Reasoning and its Applications: 
  1965 			Essays in Honor of {Larry Wos}},
  1966   booktitle	= {Automated Reasoning and its Applications: 
  1967 			Essays in Honor of {Larry Wos}},
  1968   publisher	= MIT,
  1969   year		= 1997,
  1970   editor	= {Robert Veroff}}
  1971 
  1972 @proceedings{fme93,
  1973   editor	= {J. C. P. Woodcock and P. G. Larsen},
  1974   title		= {FME '93: Industrial-Strength Formal Methods},
  1975   booktitle	= {FME '93: Industrial-Strength Formal Methods},
  1976   year		= 1993,
  1977   publisher	= Springer,
  1978   series	= LNCS,
  1979   volume        = 670}
  1980 
  1981 @Proceedings{tphols96,
  1982   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
  1983   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
  1984   editor	= {J. von Wright and J. Grundy and J. Harrison},
  1985   publisher     = Springer,
  1986   series	= LNCS,
  1987   volume        = 1125,
  1988   year		= 1996}
  1989 
  1990 @Proceedings{tphols97,
  1991   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
  1992   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
  1993   editor	= {Elsa L. Gunter and Amy Felty},
  1994   publisher     = Springer,
  1995   series	= LNCS,
  1996   volume        = 1275,
  1997   year		= 1997}
  1998 
  1999 @Proceedings{tphols98,
  2000   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
  2001   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
  2002   editor	= {Jim Grundy and Malcom Newey},
  2003   publisher     = Springer,
  2004   series	= LNCS,
  2005   volume        = 1479,
  2006   year		= 1998}
  2007 
  2008 @Proceedings{tphols99,
  2009   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
  2010   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
  2011   editor	= {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
  2012                   Paulin, C. and Thery, L.},
  2013   publisher     = Springer,
  2014   series	= LNCS,
  2015   volume        = 1690,
  2016   year		= 1999}
  2017 
  2018 @Proceedings{tphols2000,
  2019   title         = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},
  2020   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},
  2021   editor        = {J. Harrison and M. Aagaard},
  2022   publisher     = Springer,
  2023   series        = LNCS,
  2024   volume        = 1869,
  2025   year          = 2000}
  2026 
  2027 @Proceedings{tphols2001,
  2028   title         = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},
  2029   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},
  2030   editor        = {R. J. Boulton and P. B. Jackson},
  2031   publisher     = Springer,
  2032   series        = LNCS,
  2033   volume        = 2152,
  2034   year          = 2001}
  2035 
  2036 @Proceedings{ijcar2006,
  2037   title         = {Automated Reasoning: {IJCAR} 2006},
  2038   booktitle     = {Automated Reasoning: {IJCAR} 2006},
  2039   editor        = {U. Furbach and N. Shankar},
  2040   publisher     = Springer,
  2041   series        = LNCS,
  2042   volume        = 4130,
  2043   year          = 2006}
  2044 
  2045 @Proceedings{tphols2007,
  2046   title         = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},
  2047   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},
  2048   editor        = {K. Schneider and J. Brandt},
  2049   publisher     = Springer,
  2050   series        = LNCS,
  2051   volume        = 4732,
  2052   year          = 2007}
  2053 
  2054 @Proceedings{tphols2008,
  2055   title         = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},
  2056   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},
  2057   publisher     = Springer,
  2058   series        = LNCS,
  2059   year          = 2008}
  2060 %  editor        =
  2061 %  volume        = 4732,
  2062 
  2063 @Proceedings{itp2010,
  2064   title         = {Interactive Theorem Proving: {ITP}-10},
  2065   booktitle     = {Interactive Theorem Proving: {ITP}-10},
  2066   editor = "Matt Kaufmann and Lawrence Paulson",
  2067   publisher     = Springer,
  2068   series        = LNCS,
  2069   year          = 2010}
  2070 
  2071 @unpublished{classes_modules,
  2072   title         = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
  2073   author        = {Stefan Wehr et. al.}
  2074 }