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