CONTRIBUTORS
author wenzelm
Mon Oct 01 19:52:07 2007 +0200 (2007-10-01)
changeset 24799 dff164b6f2a6
parent 24333 e77ea0ea7f2c
child 24803 38577b4b1fde
permissions -rw-r--r--
misc tuning and update;
     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 
     7 Contributions to Isabelle 2007
     8 ------------------------------
     9 
    10 * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
    11     Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
    12   HOL-Word: a library for fixed-size machine words in Isabelle.
    13 
    14 * August 2007: Brian Huffman, PSU
    15   HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
    16 
    17 * June 2007: Amine Chaieb, TUM
    18   Semiring normalization and Groebner Bases.
    19   Support for dens linear orders.
    20 
    21 * June 2007: Joe Hurd, Oxford
    22   Metis theorem-prover.
    23 
    24 * 2007: Kong W. Susanto, Cambridge
    25   HOL: Metis prover integration.
    26 
    27 * 2007: Stefan Berghofer, TUM
    28   HOL: inductive predicates.
    29 
    30 * 2006/2007: Alexander Krauss, TUM
    31   HOL: function package and related theories on termination.
    32 
    33 * 2006/2007: Florian Haftmann, TUM
    34   Pure: generic code generator framework.
    35   Pure: class package.
    36   HOL: theory reorganization, code generator setup.
    37 
    38 * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and Julien
    39   Narboux, TUM
    40   HOL/Nominal package and related tools.
    41 
    42 * November 2006: Lukas Bulwahn, TUM
    43   HOL: method "lexicographic_order" for function package.
    44 
    45 * October 2006: Stefan Hohe, TUM
    46   HOL-Algebra: ideals and quotients over rings.
    47 
    48 * August 2006: Amine Chaieb, TUM
    49   Experimental support for generic reflection and reification in HOL.
    50 
    51 * July 2006: Rafal Kolanski, NICTA
    52   Hex (0xFF) and binary (0b1011) numerals.
    53 
    54 * May 2006: Klaus Aehlig, LMU
    55   Command 'normal_form': normalization by evaluation.
    56 
    57 * May 2006: Amine Chaieb, TUM
    58   HOL-Complex: Ferrante and Rackoff Algorithm for linear real
    59   arithmetic.
    60 
    61 * February 2006: Benjamin Porter, NICTA
    62   HOL and HOL-Complex: generalised mean value theorem, continuum is
    63   not denumerable, harmonic and arithmetic series, and denumerability
    64   of rationals.
    65 
    66 * October 2005: Martin Wildmoser, TUM
    67   Sketch for Isar 'guess' element.
    68 
    69 
    70 Contributions to Isabelle 2005
    71 ------------------------------
    72 
    73 * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
    74   HOL-Complex: Formalization of Taylor series.
    75 
    76 * September 2005: Stephan Merz, Alwen Tiu, QSL Loria
    77   Components for SAT solver method using zChaff.
    78 
    79 * September 2005: Ning Zhang and Christian Urban, LMU Munich
    80   A Chinese theory.
    81 
    82 * September 2005: Bernhard Haeupler, TUM
    83   Method comm_ring for proving equalities in commutative rings.
    84 
    85 * July/August 2005: Jeremy Avigad, Carnegie Mellon University
    86   Various improvements of the HOL and HOL-Complex library.
    87 
    88 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
    89   Some structured proofs about completeness of real numbers.
    90 
    91 * May 2005: Rafal Kolanski and Gerwin Klein, NICTA
    92   Improved retrieval of facts from theory/proof context.
    93 
    94 * February 2005: Lucas Dixon, University of Edinburgh
    95   Improved subst method.
    96 
    97 * 2005: Brian Huffman, OGI
    98   Various improvements of HOLCF.
    99   Some improvements of the HOL-Complex library.
   100 
   101 * 2005: Claire Quigley and Jia Meng, University of Cambridge
   102   Some support for asynchronous communication with external provers
   103   (experimental).
   104 
   105 * 2005: Florian Haftmann, TUM
   106   Contributions to document 'sugar'.
   107   Various ML combinators, notably linear functional transformations.
   108   Some cleanup of ML legacy.
   109   Additional antiquotations.
   110   Improved Isabelle web site.
   111 
   112 * 2004/2005: David Aspinall, University of Edinburgh
   113   Various elements of XML and PGIP based communication with user
   114   interfaces (experimental).
   115 
   116 * 2004/2005: Gerwin Klein, NICTA
   117   Contributions to document 'sugar'.
   118   Improved Isabelle web site.
   119   Improved HTML presentation of theories.
   120 
   121 * 2004/2005: Clemens Ballarin, TUM
   122   Provers: tools for transitive relations and quasi orders.
   123   Improved version of locales, notably interpretation of locales.
   124   Improved version of HOL-Algebra.
   125 
   126 * 2004/2005: Amine Chaieb, TUM
   127   Improved version of HOL presburger method.
   128 
   129 * 2004/2005: Steven Obua, TUM
   130   Improved version of HOL/Import, support for HOL-Light.
   131   Improved version of HOL-Complex-Matrix.
   132   Pure/defs: more sophisticated checks on well-formedness of overloading.
   133   Pure/Tools: an experimental evaluator for lambda terms.
   134 
   135 * 2004/2005: Norbert Schirmer, TUM
   136   Contributions to document 'sugar'.
   137   Improved version of HOL/record.
   138 
   139 * 2004/2005: Sebastian Skalberg, TUM
   140   Improved version of HOL/Import.
   141   Some internal ML reorganizations.
   142 
   143 * 2004/2005: Tjark Weber, TUM
   144   SAT solver method using zChaff.
   145   Improved version of HOL/refute.
   146 
   147 $Id$