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