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