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