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