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