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