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