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