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