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