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