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