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