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