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