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