CONTRIBUTORS
author blanchet
Mon Oct 26 14:21:20 2009 +0100 (2009-10-26)
changeset 33203 322d928d9f8f
parent 33182 45f6afe0a979
parent 33192 08a39a957ed7
child 33419 8ae45e87b992
permissions -rw-r--r--
merged
     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 
     7 Contributions to this Isabelle version
     8 --------------------------------------
     9 
    10 * October 2009: Jasmin Blanchette, TUM
    11   Nitpick: yet another counterexample generator for Isabelle/HOL
    12 
    13 * October 2009: Sascha Boehme, TUM
    14   Extension of SMT method: proof-reconstruction for the SMT solver Z3.
    15 
    16 * October 2009: Florian Haftmann, TUM
    17   Refinement of parts of the HOL datatype package.
    18 
    19 * October 2009: Florian Haftmann, TUM
    20   Generic term styles for term antiquotations.
    21 
    22 * September 2009: Thomas Sewell, NICTA
    23   More efficient HOL/record implementation.
    24 
    25 * September 2009: Sascha Boehme, TUM
    26   SMT method using external SMT solvers.
    27 
    28 * September 2009: Florian Haftmann, TUM
    29   Refinement of sets and lattices.
    30 
    31 * July 2009: Jeremy Avigad and Amine Chaieb
    32   New number theory.
    33 
    34 * July 2009: Philipp Meyer, TUM
    35   HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
    36   prover.
    37 
    38 * July 2009: Florian Haftmann, TUM
    39   New quickcheck implementation using new code generator.
    40 
    41 * July 2009: Florian Haftmann, TUM
    42   HOL/Library/FSet: an explicit type of sets; finite sets ready to use
    43   for code generation.
    44 
    45 * June 2009: Florian Haftmann, TUM
    46   HOL/Library/Tree: searchtrees implementing mappings, ready to use
    47   for code generation.
    48 
    49 * March 2009: Philipp Meyer, TUM
    50   Minimalization algorithm for results from sledgehammer call.
    51 
    52 
    53 Contributions to Isabelle2009
    54 -----------------------------
    55 
    56 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
    57   Cambridge
    58   Elementary topology in Euclidean space.
    59 
    60 * March 2009: Johannes Hoelzl, TUM
    61   Method "approximation", which proves real valued inequalities by
    62   computation.
    63 
    64 * February 2009: Filip Maric, Univ. of Belgrade
    65   A Serbian theory.
    66 
    67 * February 2009: Jasmin Christian Blanchette, TUM
    68   Misc cleanup of HOL/refute.
    69 
    70 * February 2009: Timothy Bourke, NICTA
    71   New find_consts command.
    72 
    73 * February 2009: Timothy Bourke, NICTA
    74   "solves" criterion for find_theorems and auto_solve option
    75 
    76 * December 2008: Clemens Ballarin, TUM
    77   New locale implementation.
    78 
    79 * December 2008: Armin Heller, TUM and Alexander Krauss, TUM
    80   Method "sizechange" for advanced termination proofs.
    81 
    82 * November 2008: Timothy Bourke, NICTA
    83   Performance improvement (factor 50) for find_theorems.
    84 
    85 * 2008: Florian Haftmann, TUM
    86   Various extensions and restructurings in HOL, improvements
    87   in evaluation mechanisms, new module binding.ML for name bindings.
    88 
    89 * October 2008: Fabian Immler, TUM
    90   ATP manager for Sledgehammer, based on ML threads instead of Posix
    91   processes.  Additional ATP wrappers, including remote SystemOnTPTP
    92   services.
    93 
    94 * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen
    95   Prover for coherent logic.
    96 
    97 * August 2008: Fabian Immler, TUM
    98   Vampire wrapper script for remote SystemOnTPTP service.
    99 
   100 
   101 Contributions to Isabelle2008
   102 -----------------------------
   103 
   104 * 2007/2008:
   105   Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
   106   HOL library improvements.
   107 
   108 * 2007/2008: Brian Huffman, PSU
   109   HOLCF library improvements.
   110 
   111 * 2007/2008: Stefan Berghofer, TUM
   112   HOL-Nominal package improvements.
   113 
   114 * March 2008: Markus Reiter, TUM
   115   HOL/Library/RBT: red-black trees.
   116 
   117 * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and
   118   Lukas Bulwahn, TUM and John Matthews, Galois:
   119   HOL/Library/Imperative_HOL: Haskell-style imperative data structures
   120   for HOL.
   121 
   122 * December 2007: Norbert Schirmer, Uni Saarbruecken
   123   Misc improvements of record package in HOL.
   124 
   125 * December 2007: Florian Haftmann, TUM
   126   Overloading and class instantiation target.
   127 
   128 * December 2007: Florian Haftmann, TUM
   129   New version of primrec package for local theories.
   130 
   131 * December 2007: Alexander Krauss, TUM
   132   Method "induction_scheme" in HOL.
   133 
   134 * November 2007: Peter Lammich, Uni Muenster
   135   HOL-Lattice: some more lemmas.
   136 
   137 
   138 Contributions to Isabelle2007
   139 -----------------------------
   140 
   141 * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken
   142   State Spaces: The Locale Way (in HOL).
   143 
   144 * October 2007: Mark A. Hillebrand, DFKI
   145   Robust sub/superscripts in LaTeX document output.
   146 
   147 * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
   148     Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
   149   HOL-Word: a library for fixed-size machine words in Isabelle.
   150 
   151 * August 2007: Brian Huffman, PSU
   152   HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
   153 
   154 * June 2007: Amine Chaieb, TUM
   155   Semiring normalization and Groebner Bases.
   156   Support for dense linear orders.
   157 
   158 * June 2007: Joe Hurd, Oxford
   159   Metis theorem-prover.
   160 
   161 * 2007: Kong W. Susanto, Cambridge
   162   HOL: Metis prover integration.
   163 
   164 * 2007: Stefan Berghofer, TUM
   165   HOL: inductive predicates and sets.
   166 
   167 * 2007: Norbert Schirmer, TUM
   168   HOL/record: misc improvements.
   169 
   170 * 2006/2007: Alexander Krauss, TUM
   171   HOL: function package and related theories on termination.
   172 
   173 * 2006/2007: Florian Haftmann, TUM
   174   Pure: generic code generator framework.
   175   Pure: class package.
   176   HOL: theory reorganization, code generator setup.
   177 
   178 * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and
   179     Julien Narboux, TUM
   180   HOL/Nominal package and related tools.
   181 
   182 * November 2006: Lukas Bulwahn, TUM
   183   HOL: method "lexicographic_order" for function package.
   184 
   185 * October 2006: Stefan Hohe, TUM
   186   HOL-Algebra: ideals and quotients over rings.
   187 
   188 * August 2006: Amine Chaieb, TUM
   189   Experimental support for generic reflection and reification in HOL.
   190 
   191 * July 2006: Rafal Kolanski, NICTA
   192   Hex (0xFF) and binary (0b1011) numerals.
   193 
   194 * May 2006: Klaus Aehlig, LMU
   195   Command 'normal_form': normalization by evaluation.
   196 
   197 * May 2006: Amine Chaieb, TUM
   198   HOL-Complex: Ferrante and Rackoff Algorithm for linear real
   199   arithmetic.
   200 
   201 * February 2006: Benjamin Porter, NICTA
   202   HOL and HOL-Complex: generalised mean value theorem, continuum is
   203   not denumerable, harmonic and arithmetic series, and denumerability
   204   of rationals.
   205 
   206 * October 2005: Martin Wildmoser, TUM
   207   Sketch for Isar 'guess' element.
   208 
   209 
   210 Contributions to Isabelle2005
   211 -----------------------------
   212 
   213 * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
   214   HOL-Complex: Formalization of Taylor series.
   215 
   216 * September 2005: Stephan Merz, Alwen Tiu, QSL Loria
   217   Components for SAT solver method using zChaff.
   218 
   219 * September 2005: Ning Zhang and Christian Urban, LMU Munich
   220   A Chinese theory.
   221 
   222 * September 2005: Bernhard Haeupler, TUM
   223   Method comm_ring for proving equalities in commutative rings.
   224 
   225 * July/August 2005: Jeremy Avigad, Carnegie Mellon University
   226   Various improvements of the HOL and HOL-Complex library.
   227 
   228 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
   229   Some structured proofs about completeness of real numbers.
   230 
   231 * May 2005: Rafal Kolanski and Gerwin Klein, NICTA
   232   Improved retrieval of facts from theory/proof context.
   233 
   234 * February 2005: Lucas Dixon, University of Edinburgh
   235   Improved subst method.
   236 
   237 * 2005: Brian Huffman, OGI
   238   Various improvements of HOLCF.
   239   Some improvements of the HOL-Complex library.
   240 
   241 * 2005: Claire Quigley and Jia Meng, University of Cambridge
   242   Some support for asynchronous communication with external provers
   243   (experimental).
   244 
   245 * 2005: Florian Haftmann, TUM
   246   Contributions to document 'sugar'.
   247   Various ML combinators, notably linear functional transformations.
   248   Some cleanup of ML legacy.
   249   Additional antiquotations.
   250   Improved Isabelle web site.
   251 
   252 * 2004/2005: David Aspinall, University of Edinburgh
   253   Various elements of XML and PGIP based communication with user
   254   interfaces (experimental).
   255 
   256 * 2004/2005: Gerwin Klein, NICTA
   257   Contributions to document 'sugar'.
   258   Improved Isabelle web site.
   259   Improved HTML presentation of theories.
   260 
   261 * 2004/2005: Clemens Ballarin, TUM
   262   Provers: tools for transitive relations and quasi orders.
   263   Improved version of locales, notably interpretation of locales.
   264   Improved version of HOL-Algebra.
   265 
   266 * 2004/2005: Amine Chaieb, TUM
   267   Improved version of HOL presburger method.
   268 
   269 * 2004/2005: Steven Obua, TUM
   270   Improved version of HOL/Import, support for HOL-Light.
   271   Improved version of HOL-Complex-Matrix.
   272   Pure/defs: more sophisticated checks on well-formedness of overloading.
   273   Pure/Tools: an experimental evaluator for lambda terms.
   274 
   275 * 2004/2005: Norbert Schirmer, TUM
   276   Contributions to document 'sugar'.
   277   Improved version of HOL/record.
   278 
   279 * 2004/2005: Sebastian Skalberg, TUM
   280   Improved version of HOL/Import.
   281   Some internal ML reorganizations.
   282 
   283 * 2004/2005: Tjark Weber, TUM
   284   SAT solver method using zChaff.
   285   Improved version of HOL/refute.