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