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