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