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