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