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