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