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