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