CONTRIBUTORS
author kleing
Mon Aug 20 04:34:31 2007 +0200 (2007-08-20)
changeset 24333 e77ea0ea7f2c
parent 24332 e3a2b75b1cf9
child 24799 dff164b6f2a6
permissions -rw-r--r--
* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.

* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution
kleing@23382
     1
For the purposes of the license agreement in the file COPYRIGHT, a 
kleing@23382
     2
'contributor' is anybody who is listed in this file (CONTRIBUTORS) or 
kleing@23382
     3
who is listed as an author in one of the source files of this Isabelle
kleing@23382
     4
distribution.
kleing@23382
     5
wenzelm@20340
     6
wenzelm@23252
     7
Contributions to Isabelle 2007
wenzelm@23252
     8
------------------------------
wenzelm@23252
     9
kleing@24333
    10
* August 2007: Jeremy Dawson, NICTA,
kleing@24333
    11
               Paul Graunke, Galois, 
kleing@24333
    12
               Brian Huffman, PSU,
kleing@24333
    13
               Gerwin Klein, NICTA, 
kleing@24333
    14
               John Matthews, Galois
kleing@24333
    15
  HOL-Word: a library for fixed-size machine words in Isabelle.
kleing@24333
    16
kleing@24332
    17
* August 2007: Brian Huffman, PSU
kleing@24332
    18
  HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type
kleing@24332
    19
wenzelm@23252
    20
* June 2007: Amine Chaieb, TUM
wenzelm@23252
    21
  Semiring normalization and Groebner Bases
wenzelm@17866
    22
paulson@23449
    23
* June 2007: Joe Hurd, Oxford
paulson@23449
    24
  Metis theorem-prover
paulson@23449
    25
paulson@23449
    26
* 2006/2007: Kong W. Susanto, Cambridge
paulson@23449
    27
  HOL: Metis prover integration.
paulson@23449
    28
haftmann@22449
    29
* 2006/2007: Florian Haftmann, TUM
haftmann@22449
    30
  Pure: generic code generator framework.
haftmann@22449
    31
  Pure: class package.
haftmann@22449
    32
  HOL: theory tuning, code generator setup.
haftmann@22449
    33
wenzelm@21242
    34
* November 2006: Lukas Bulwahn, TUM
wenzelm@21242
    35
  HOL/function: method "lexicographic_order".
wenzelm@21242
    36
wenzelm@21169
    37
* October 2006: Stefan Hohe, TUM
wenzelm@21169
    38
  HOL-Algebra: ideals and quotients over rings.
wenzelm@21169
    39
wenzelm@20340
    40
* August 2006: Amine Chaieb, TUM
wenzelm@20340
    41
  Experimental support for generic reflection and reification in HOL.
wenzelm@20340
    42
kleing@20067
    43
* July 2006: Rafal Kolanski, NICTA
kleing@20067
    44
  Hex (0xFF) and binary (0b1011) numerals.
kleing@20067
    45
nipkow@19896
    46
* May 2006: Klaus Aehlig, LMU
nipkow@19896
    47
  Command 'normal_form': normalization by evaluation.
nipkow@19896
    48
wenzelm@19650
    49
* May 2006: Amine Chaieb, TUM
wenzelm@19650
    50
  HOL-Complex: Ferrante and Rackoff Algorithm for linear real
wenzelm@19650
    51
  arithmetic.
kleing@19470
    52
kleing@19470
    53
* February 2006: Benjamin Porter, NICTA
kleing@23382
    54
  HOL and HOL-Complex: generalised mean value theorem, continuum is
kleing@19470
    55
  not denumerable, harmonic and arithmetic series, and denumerability
kleing@19470
    56
  of rationals.
wenzelm@17532
    57
wenzelm@19650
    58
* October 2005: Martin Wildmoser, TUM
wenzelm@19650
    59
  Sketch for Isar 'guess' element.
wenzelm@19650
    60
wenzelm@19650
    61
wenzelm@17532
    62
Contributions to Isabelle 2005
wenzelm@17532
    63
------------------------------
wenzelm@17382
    64
wenzelm@17640
    65
* September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
wenzelm@17640
    66
  HOL-Complex: Formalization of Taylor series.
wenzelm@17640
    67
wenzelm@17640
    68
* September 2005: Stephan Merz, Alwen Tiu, QSL Loria
wenzelm@17640
    69
  Components for SAT solver method using zChaff.
wenzelm@17640
    70
wenzelm@17534
    71
* September 2005: Ning Zhang and Christian Urban, LMU Munich
wenzelm@17534
    72
  A Chinese theory.
wenzelm@17534
    73
wenzelm@17562
    74
* September 2005: Bernhard Haeupler, TUM
wenzelm@17382
    75
  Method comm_ring for proving equalities in commutative rings.
wenzelm@16892
    76
wenzelm@17532
    77
* July/August 2005: Jeremy Avigad, Carnegie Mellon University
wenzelm@16892
    78
  Various improvements of the HOL and HOL-Complex library.
wenzelm@16868
    79
wenzelm@16892
    80
* July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
wenzelm@16892
    81
  Some structured proofs about completeness of real numbers.
wenzelm@16892
    82
wenzelm@17532
    83
* May 2005: Rafal Kolanski and Gerwin Klein, NICTA
wenzelm@17532
    84
  Improved retrieval of facts from theory/proof context.
wenzelm@15994
    85
wenzelm@16252
    86
* February 2005: Lucas Dixon, University of Edinburgh
wenzelm@17532
    87
  Improved subst method.
wenzelm@17532
    88
wenzelm@17532
    89
* 2005: Brian Huffman, OGI
wenzelm@17532
    90
  Various improvements of HOLCF.
wenzelm@17532
    91
  Some improvements of the HOL-Complex library.
wenzelm@17532
    92
wenzelm@17532
    93
* 2005: Claire Quigley and Jia Meng, University of Cambridge
wenzelm@17532
    94
  Some support for asynchronous communication with external provers
wenzelm@17532
    95
  (experimental).
wenzelm@17532
    96
wenzelm@17532
    97
* 2005: Florian Haftmann, TUM
wenzelm@17543
    98
  Contributions to document 'sugar'.
wenzelm@17532
    99
  Various ML combinators, notably linear functional transformations.
wenzelm@17532
   100
  Some cleanup of ML legacy.
wenzelm@17532
   101
  Additional antiquotations.
wenzelm@17532
   102
  Improved Isabelle web site.
wenzelm@17532
   103
wenzelm@17532
   104
* 2004/2005: David Aspinall, University of Edinburgh
wenzelm@17532
   105
  Various elements of XML and PGIP based communication with user
wenzelm@17532
   106
  interfaces (experimental).
wenzelm@17532
   107
wenzelm@17532
   108
* 2004/2005: Gerwin Klein, NICTA
wenzelm@17532
   109
  Contributions to document 'sugar'.
wenzelm@17532
   110
  Improved Isabelle web site.
wenzelm@17532
   111
  Improved HTML presentation of theories.
wenzelm@17532
   112
wenzelm@17532
   113
* 2004/2005: Clemens Ballarin, TUM
wenzelm@17532
   114
  Provers: tools for transitive relations and quasi orders.
wenzelm@17532
   115
  Improved version of locales, notably interpretation of locales.
wenzelm@17532
   116
  Improved version of HOL-Algebra.
wenzelm@17532
   117
wenzelm@17532
   118
* 2004/2005: Amine Chaieb, TUM
wenzelm@17532
   119
  Improved version of HOL presburger method.
wenzelm@17532
   120
wenzelm@17532
   121
* 2004/2005: Steven Obua, TUM
wenzelm@17532
   122
  Improved version of HOL/Import, support for HOL-Light.
wenzelm@17532
   123
  Improved version of HOL-Complex-Matrix.
wenzelm@17572
   124
  Pure/defs: more sophisticated checks on well-formedness of overloading.
wenzelm@17543
   125
  Pure/Tools: an experimental evaluator for lambda terms.
wenzelm@17532
   126
wenzelm@17532
   127
* 2004/2005: Norbert Schirmer, TUM
wenzelm@17532
   128
  Contributions to document 'sugar'.
wenzelm@17532
   129
  Improved version of HOL/record.
wenzelm@17532
   130
wenzelm@17532
   131
* 2004/2005: Sebastian Skalberg, TUM
wenzelm@17532
   132
  Improved version of HOL/Import.
wenzelm@17532
   133
  Some internal ML reorganizations.
wenzelm@17532
   134
wenzelm@17532
   135
* 2004/2005: Tjark Weber, TUM
wenzelm@17640
   136
  SAT solver method using zChaff.
wenzelm@17532
   137
  Improved version of HOL/refute.
wenzelm@16252
   138
wenzelm@15994
   139
$Id$