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