CONTRIBUTORS
author wenzelm
Sun Sep 29 13:53:16 2013 +0200 (2013-09-29)
changeset 53984 b9139b14c1c5
parent 53978 65c893e0849f
child 54010 5ac1495fed4e
permissions -rw-r--r--
updated for release;
     1 For the purposes of the license agreement in the file COPYRIGHT, a
     2 'contributor' is anybody who is listed in this file (CONTRIBUTORS) or
     3 who is listed as an author in one of the source files of this Isabelle
     4 distribution.
     5 
     6 Contributions to Isabelle2013-1
     7 -------------------------------
     8 
     9 * September 2013: Nik Sultana, University of Cambridge
    10   Improvements to HOL/TPTP parser and import facilities.
    11 
    12 * Summer 2013: Makarius Wenzel, Université Paris-Sud / LRI
    13   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
    14 
    15 * Summer 2013: Manuel Eberl, TUM
    16   Generation of elimination rules in the function package.
    17   New command "fun_cases".
    18 
    19 * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and
    20   Jasmin Blanchette, TUM
    21   Various improvements to BNF-based (co)datatype package, including
    22   "primrec_new" and "primcorecursive" commands and a compatibility
    23   layer.
    24 
    25 * Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen
    26   Jasmin Blanchette, TUM
    27   Various improvements to MaSh, including a server mode.
    28 
    29 * First half of 2013: Steffen Smolka, TUM
    30   Further improvements to Sledgehammer's Isar proof generator.
    31 
    32 * Summer 2013: Christian Sternagel, JAIST
    33   Improved support for ad hoc overloading of constants, including
    34   documentation and examples.
    35 
    36 * May 2013: Florian Haftmann, TUM
    37   Ephemeral interpretation in local theories.
    38 
    39 * May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM
    40   Spec_Check: A Quickcheck tool for Isabelle/ML.
    41 
    42 * April 2013: Stefan Berghofer, secunet Security Networks AG
    43   Dmitriy Traytel, TUM
    44   Makarius Wenzel, Université Paris-Sud / LRI
    45   Case translations as a separate check phase independent of the
    46   datatype package.
    47 
    48 * March 2013: Florian Haftmann, TUM
    49   Reform of "big operators" on sets.
    50 
    51 * March 2013: Florian Haftmann, TUM
    52   Algebraic locale hierarchy for orderings and (semi)lattices.
    53 
    54 * February 2013: Florian Haftmann, TUM
    55   Reworking and consolidation of code generation for target language
    56   numerals.
    57 
    58 * February 2013: Florian Haftmann, TUM
    59   Sieve of Eratosthenes.
    60 
    61 
    62 Contributions to Isabelle2013
    63 -----------------------------
    64 
    65 * 2012: Makarius Wenzel, Université Paris-Sud / LRI
    66   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
    67 
    68 * Fall 2012: Daniel Kühlwein, ICIS, Radboud University Nijmegen
    69   Jasmin Blanchette, TUM
    70   Implemented Machine Learning for Sledgehammer (MaSh).
    71 
    72 * Fall 2012: Steffen Smolka, TUM
    73   Various improvements to Sledgehammer's Isar proof generator,
    74   including a smart type annotation algorithm and proof shrinking.
    75 
    76 * December 2012: Alessandro Coglio, Kestrel
    77   Contributions to HOL's Lattice library.
    78 
    79 * November 2012: Fabian Immler, TUM
    80   "Symbols" dockable for Isabelle/jEdit.
    81 
    82 * November 2012: Fabian Immler, TUM
    83   Proof of the Daniell-Kolmogorov theorem: the existence of the limit
    84   of projective families.
    85 
    86 * October 2012: Andreas Lochbihler, KIT
    87   Efficient construction of red-black trees from sorted associative
    88   lists.
    89 
    90 * September 2012: Florian Haftmann, TUM
    91   Lattice instances for type option.
    92 
    93 * September 2012: Christian Sternagel, JAIST
    94   Consolidated HOL/Library (theories: Prefix_Order, Sublist, and
    95   Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists.
    96 
    97 * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM
    98   New BNF-based (co)datatype package.
    99 
   100 * August 2012: Andrei Popescu and Dmitriy Traytel, TUM
   101   Theories of ordinals and cardinals.
   102 
   103 * July 2012: Makarius Wenzel, Université Paris-Sud / LRI
   104   Advanced support for Isabelle sessions and build management, notably
   105   "isabelle build".
   106 
   107 * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
   108   Simproc for rewriting set comprehensions into pointfree expressions.
   109 
   110 * May 2012: Andreas Lochbihler, KIT
   111   Theory of almost everywhere constant functions.
   112 
   113 * 2010-2012: Markus Kaiser and Lukas Bulwahn, TUM
   114   Graphview in Scala/Swing.
   115 
   116 
   117 Contributions to Isabelle2012
   118 -----------------------------
   119 
   120 * April 2012: Johannes Hölzl, TUM
   121   Probability: Introduced type to represent measures instead of
   122   locales.
   123 
   124 * April 2012: Johannes Hölzl, Fabian Immler, TUM
   125   Float: Moved to Dyadic rationals to represent floating point numers.
   126 
   127 * April 2012: Thomas Sewell, NICTA and
   128   2010: Sascha Boehme, TUM
   129   Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector
   130   equalities/inequalities.
   131 
   132 * March 2012: Christian Sternagel, JAIST
   133   Consolidated theory of relation composition.
   134 
   135 * March 2012: Nik Sultana, University of Cambridge
   136   HOL/TPTP parser and import facilities.
   137 
   138 * March 2012: Cezary Kaliszyk, University of Innsbruck and
   139   Alexander Krauss, QAware GmbH
   140   Faster and more scalable Import mechanism for HOL Light proofs.
   141 
   142 * January 2012: Florian Haftmann, TUM, et al.
   143   (Re-)Introduction of the "set" type constructor.
   144 
   145 * 2012: Ondrej Kuncar, TUM
   146   New package Lifting, various improvements and refinements to the
   147   Quotient package.
   148 
   149 * 2011/2012: Jasmin Blanchette, TUM
   150   Various improvements to Sledgehammer, notably: tighter integration
   151   with SPASS, support for more provers (Alt-Ergo, iProver,
   152   iProver-Eq).
   153 
   154 * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI
   155   Various refinements of local theory infrastructure.
   156   Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE.
   157 
   158 
   159 Contributions to Isabelle2011-1
   160 -------------------------------
   161 
   162 * September 2011: Peter Gammie
   163   Theory HOL/Library/Saturated: numbers with saturated arithmetic.
   164 
   165 * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
   166   Refined theory on complete lattices.
   167 
   168 * August 2011: Brian Huffman, Portland State University
   169   Miscellaneous cleanup of Complex_Main and Multivariate_Analysis.
   170 
   171 * June 2011: Brian Huffman, Portland State University
   172   Proof method "countable_datatype" for theory Library/Countable.
   173 
   174 * 2011: Jasmin Blanchette, TUM
   175   Various improvements to Sledgehammer, notably: use of sound
   176   translations, support for more provers (Waldmeister, LEO-II,
   177   Satallax). Further development of Nitpick and 'try' command.
   178 
   179 * 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
   180   Theory HOL/Library/Cset_Monad allows do notation for computable sets
   181   (cset) via the generic monad ad-hoc overloading facility.
   182 
   183 * 2011: Johannes Hölzl, Armin Heller, TUM and
   184   Bogdan Grechuk, University of Edinburgh
   185   Theory HOL/Library/Extended_Reals: real numbers extended with plus
   186   and minus infinity.
   187 
   188 * 2011: Makarius Wenzel, Université Paris-Sud / LRI
   189   Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
   190   Prover IDE.
   191 
   192 
   193 Contributions to Isabelle2011
   194 -----------------------------
   195 
   196 * January 2011: Stefan Berghofer, secunet Security Networks AG
   197   HOL-SPARK: an interactive prover back-end for SPARK.
   198 
   199 * October 2010: Bogdan Grechuk, University of Edinburgh
   200   Extended convex analysis in Multivariate Analysis.
   201 
   202 * October 2010: Dmitriy Traytel, TUM
   203   Coercive subtyping via subtype constraints.
   204 
   205 * October 2010: Alexander Krauss, TUM
   206   Command partial_function for function definitions based on complete
   207   partial orders in HOL.
   208 
   209 * September 2010: Florian Haftmann, TUM
   210   Refined concepts for evaluation, i.e., normalization of terms using
   211   different techniques.
   212 
   213 * September 2010: Florian Haftmann, TUM
   214   Code generation for Scala.
   215 
   216 * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
   217   Improved Probability theory in HOL.
   218 
   219 * July 2010: Florian Haftmann, TUM
   220   Reworking and extension of the Imperative HOL framework.
   221 
   222 * July 2010: Alexander Krauss, TUM and Christian Sternagel, University
   223     of Innsbruck
   224   Ad-hoc overloading. Generic do notation for monads.
   225 
   226 
   227 Contributions to Isabelle2009-2
   228 -------------------------------
   229 
   230 * 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM,
   231   Makarius Wenzel, TUM / LRI
   232   Elimination of type classes from proof terms.
   233 
   234 * April 2010: Florian Haftmann, TUM
   235   Reorganization of abstract algebra type classes.
   236 
   237 * April 2010: Florian Haftmann, TUM
   238   Code generation for data representations involving invariants;
   239   various collections avaiable in theories Fset, Dlist, RBT,
   240   Mapping and AssocList.
   241 
   242 * March 2010: Sascha Boehme, TUM
   243   Efficient SHA1 library for Poly/ML.
   244 
   245 * February 2010: Cezary Kaliszyk and Christian Urban, TUM
   246   Quotient type package for Isabelle/HOL.
   247 
   248 
   249 Contributions to Isabelle2009-1
   250 -------------------------------
   251 
   252 * November 2009, Brian Huffman, PSU
   253   New definitional domain package for HOLCF.
   254 
   255 * November 2009: Robert Himmelmann, TUM
   256   Derivation and Brouwer's fixpoint theorem in Multivariate Analysis.
   257 
   258 * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
   259   A tabled implementation of the reflexive transitive closure.
   260 
   261 * November 2009: Lukas Bulwahn, TUM
   262   Predicate Compiler: a compiler for inductive predicates to
   263   equational specifications.
   264 
   265 * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris
   266   HOL-Boogie: an interactive prover back-end for Boogie and VCC.
   267 
   268 * October 2009: Jasmin Blanchette, TUM
   269   Nitpick: yet another counterexample generator for Isabelle/HOL.
   270 
   271 * October 2009: Sascha Boehme, TUM
   272   Extension of SMT method: proof-reconstruction for the SMT solver Z3.
   273 
   274 * October 2009: Florian Haftmann, TUM
   275   Refinement of parts of the HOL datatype package.
   276 
   277 * October 2009: Florian Haftmann, TUM
   278   Generic term styles for term antiquotations.
   279 
   280 * September 2009: Thomas Sewell, NICTA
   281   More efficient HOL/record implementation.
   282 
   283 * September 2009: Sascha Boehme, TUM
   284   SMT method using external SMT solvers.
   285 
   286 * September 2009: Florian Haftmann, TUM
   287   Refinement of sets and lattices.
   288 
   289 * July 2009: Jeremy Avigad and Amine Chaieb
   290   New number theory.
   291 
   292 * July 2009: Philipp Meyer, TUM
   293   HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
   294   prover.
   295 
   296 * July 2009: Florian Haftmann, TUM
   297   New quickcheck implementation using new code generator.
   298 
   299 * July 2009: Florian Haftmann, TUM
   300   HOL/Library/Fset: an explicit type of sets; finite sets ready to use
   301   for code generation.
   302 
   303 * June 2009: Florian Haftmann, TUM
   304   HOL/Library/Tree: search trees implementing mappings, ready to use
   305   for code generation.
   306 
   307 * March 2009: Philipp Meyer, TUM
   308   Minimization tool for results from Sledgehammer.
   309 
   310 
   311 Contributions to Isabelle2009
   312 -----------------------------
   313 
   314 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
   315   Cambridge
   316   Elementary topology in Euclidean space.
   317 
   318 * March 2009: Johannes Hoelzl, TUM
   319   Method "approximation", which proves real valued inequalities by
   320   computation.
   321 
   322 * February 2009: Filip Maric, Univ. of Belgrade
   323   A Serbian theory.
   324 
   325 * February 2009: Jasmin Christian Blanchette, TUM
   326   Misc cleanup of HOL/refute.
   327 
   328 * February 2009: Timothy Bourke, NICTA
   329   New find_consts command.
   330 
   331 * February 2009: Timothy Bourke, NICTA
   332   "solves" criterion for find_theorems and auto_solve option
   333 
   334 * December 2008: Clemens Ballarin, TUM
   335   New locale implementation.
   336 
   337 * December 2008: Armin Heller, TUM and Alexander Krauss, TUM
   338   Method "sizechange" for advanced termination proofs.
   339 
   340 * November 2008: Timothy Bourke, NICTA
   341   Performance improvement (factor 50) for find_theorems.
   342 
   343 * 2008: Florian Haftmann, TUM
   344   Various extensions and restructurings in HOL, improvements
   345   in evaluation mechanisms, new module binding.ML for name bindings.
   346 
   347 * October 2008: Fabian Immler, TUM
   348   ATP manager for Sledgehammer, based on ML threads instead of Posix
   349   processes.  Additional ATP wrappers, including remote SystemOnTPTP
   350   services.
   351 
   352 * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen
   353   Prover for coherent logic.
   354 
   355 * August 2008: Fabian Immler, TUM
   356   Vampire wrapper script for remote SystemOnTPTP service.
   357 
   358 
   359 Contributions to Isabelle2008
   360 -----------------------------
   361 
   362 * 2007/2008:
   363   Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
   364   HOL library improvements.
   365 
   366 * 2007/2008: Brian Huffman, PSU
   367   HOLCF library improvements.
   368 
   369 * 2007/2008: Stefan Berghofer, TUM
   370   HOL-Nominal package improvements.
   371 
   372 * March 2008: Markus Reiter, TUM
   373   HOL/Library/RBT: red-black trees.
   374 
   375 * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and
   376   Lukas Bulwahn, TUM and John Matthews, Galois:
   377   HOL/Library/Imperative_HOL: Haskell-style imperative data structures
   378   for HOL.
   379 
   380 * December 2007: Norbert Schirmer, Uni Saarbruecken
   381   Misc improvements of record package in HOL.
   382 
   383 * December 2007: Florian Haftmann, TUM
   384   Overloading and class instantiation target.
   385 
   386 * December 2007: Florian Haftmann, TUM
   387   New version of primrec package for local theories.
   388 
   389 * December 2007: Alexander Krauss, TUM
   390   Method "induction_scheme" in HOL.
   391 
   392 * November 2007: Peter Lammich, Uni Muenster
   393   HOL-Lattice: some more lemmas.
   394 
   395 
   396 Contributions to Isabelle2007
   397 -----------------------------
   398 
   399 * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken
   400   State Spaces: The Locale Way (in HOL).
   401 
   402 * October 2007: Mark A. Hillebrand, DFKI
   403   Robust sub/superscripts in LaTeX document output.
   404 
   405 * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
   406     Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
   407   HOL-Word: a library for fixed-size machine words in Isabelle.
   408 
   409 * August 2007: Brian Huffman, PSU
   410   HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
   411 
   412 * June 2007: Amine Chaieb, TUM
   413   Semiring normalization and Groebner Bases.
   414   Support for dense linear orders.
   415 
   416 * June 2007: Joe Hurd, Oxford
   417   Metis theorem-prover.
   418 
   419 * 2007: Kong W. Susanto, Cambridge
   420   HOL: Metis prover integration.
   421 
   422 * 2007: Stefan Berghofer, TUM
   423   HOL: inductive predicates and sets.
   424 
   425 * 2007: Norbert Schirmer, TUM
   426   HOL/record: misc improvements.
   427 
   428 * 2006/2007: Alexander Krauss, TUM
   429   HOL: function package and related theories on termination.
   430 
   431 * 2006/2007: Florian Haftmann, TUM
   432   Pure: generic code generator framework.
   433   Pure: class package.
   434   HOL: theory reorganization, code generator setup.
   435 
   436 * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and
   437     Julien Narboux, TUM
   438   HOL/Nominal package and related tools.
   439 
   440 * November 2006: Lukas Bulwahn, TUM
   441   HOL: method "lexicographic_order" for function package.
   442 
   443 * October 2006: Stefan Hohe, TUM
   444   HOL-Algebra: ideals and quotients over rings.
   445 
   446 * August 2006: Amine Chaieb, TUM
   447   Experimental support for generic reflection and reification in HOL.
   448 
   449 * July 2006: Rafal Kolanski, NICTA
   450   Hex (0xFF) and binary (0b1011) numerals.
   451 
   452 * May 2006: Klaus Aehlig, LMU
   453   Command 'normal_form': normalization by evaluation.
   454 
   455 * May 2006: Amine Chaieb, TUM
   456   HOL-Complex: Ferrante and Rackoff Algorithm for linear real
   457   arithmetic.
   458 
   459 * February 2006: Benjamin Porter, NICTA
   460   HOL and HOL-Complex: generalised mean value theorem, continuum is
   461   not denumerable, harmonic and arithmetic series, and denumerability
   462   of rationals.
   463 
   464 * October 2005: Martin Wildmoser, TUM
   465   Sketch for Isar 'guess' element.
   466 
   467 
   468 Contributions to Isabelle2005
   469 -----------------------------
   470 
   471 * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
   472   HOL-Complex: Formalization of Taylor series.
   473 
   474 * September 2005: Stephan Merz, Alwen Tiu, QSL Loria
   475   Components for SAT solver method using zChaff.
   476 
   477 * September 2005: Ning Zhang and Christian Urban, LMU Munich
   478   A Chinese theory.
   479 
   480 * September 2005: Bernhard Haeupler, TUM
   481   Method comm_ring for proving equalities in commutative rings.
   482 
   483 * July/August 2005: Jeremy Avigad, Carnegie Mellon University
   484   Various improvements of the HOL and HOL-Complex library.
   485 
   486 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
   487   Some structured proofs about completeness of real numbers.
   488 
   489 * May 2005: Rafal Kolanski and Gerwin Klein, NICTA
   490   Improved retrieval of facts from theory/proof context.
   491 
   492 * February 2005: Lucas Dixon, University of Edinburgh
   493   Improved subst method.
   494 
   495 * 2005: Brian Huffman, OGI
   496   Various improvements of HOLCF.
   497   Some improvements of the HOL-Complex library.
   498 
   499 * 2005: Claire Quigley and Jia Meng, University of Cambridge
   500   Some support for asynchronous communication with external provers
   501   (experimental).
   502 
   503 * 2005: Florian Haftmann, TUM
   504   Contributions to document 'sugar'.
   505   Various ML combinators, notably linear functional transformations.
   506   Some cleanup of ML legacy.
   507   Additional antiquotations.
   508   Improved Isabelle web site.
   509 
   510 * 2004/2005: David Aspinall, University of Edinburgh
   511   Various elements of XML and PGIP based communication with user
   512   interfaces (experimental).
   513 
   514 * 2004/2005: Gerwin Klein, NICTA
   515   Contributions to document 'sugar'.
   516   Improved Isabelle web site.
   517   Improved HTML presentation of theories.
   518 
   519 * 2004/2005: Clemens Ballarin, TUM
   520   Provers: tools for transitive relations and quasi orders.
   521   Improved version of locales, notably interpretation of locales.
   522   Improved version of HOL-Algebra.
   523 
   524 * 2004/2005: Amine Chaieb, TUM
   525   Improved version of HOL presburger method.
   526 
   527 * 2004/2005: Steven Obua, TUM
   528   Improved version of HOL/Import, support for HOL-Light.
   529   Improved version of HOL-Complex-Matrix.
   530   Pure/defs: more sophisticated checks on well-formedness of overloading.
   531   Pure/Tools: an experimental evaluator for lambda terms.
   532 
   533 * 2004/2005: Norbert Schirmer, TUM
   534   Contributions to document 'sugar'.
   535   Improved version of HOL/record.
   536 
   537 * 2004/2005: Sebastian Skalberg, TUM
   538   Improved version of HOL/Import.
   539   Some internal ML reorganizations.
   540 
   541 * 2004/2005: Tjark Weber, TUM
   542   SAT solver method using zChaff.
   543   Improved version of HOL/refute.