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