CONTRIBUTORS
author haftmann
Sat Mar 23 17:11:06 2013 +0100 (2013-03-23)
changeset 51487 f4bfdee99304
parent 51173 3cbb4e95a565
child 51489 f738e6dbd844
permissions -rw-r--r--
locales for abstract orders
     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 * March 2013: Florian Haftmann, TUM
    10   Algebraic locale hierarchy for orderings and (semi)lattices.
    11 
    12 * Feb. 2013: Florian Haftmann, TUM
    13   Reworking and consolidation of code generation for target
    14   language numerals.
    15 
    16 * Feb. 2013: Florian Haftmann, TUM
    17   Sieve of Eratosthenes.
    18 
    19 
    20 Contributions to Isabelle2013
    21 -----------------------------
    22 
    23 * 2012: Makarius Wenzel, Université Paris-Sud / LRI
    24   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
    25 
    26 * Fall 2012: Daniel Kühlwein, ICIS, Radboud University Nijmegen
    27   Jasmin Blanchette, TUM
    28   Implemented Machine Learning for Sledgehammer (MaSh).
    29 
    30 * Fall 2012: Steffen Smolka, TUM
    31   Various improvements to Sledgehammer's Isar proof generator,
    32   including a smart type annotation algorithm and proof shrinking.
    33 
    34 * December 2012: Alessandro Coglio, Kestrel
    35   Contributions to HOL's Lattice library.
    36 
    37 * November 2012: Fabian Immler, TUM
    38   "Symbols" dockable for Isabelle/jEdit.
    39 
    40 * November 2012: Fabian Immler, TUM
    41   Proof of the Daniell-Kolmogorov theorem: the existence of the limit
    42   of projective families.
    43 
    44 * October 2012: Andreas Lochbihler, KIT
    45   Efficient construction of red-black trees from sorted associative
    46   lists.
    47 
    48 * September 2012: Florian Haftmann, TUM
    49   Lattice instances for type option.
    50 
    51 * September 2012: Christian Sternagel, JAIST
    52   Consolidated HOL/Library (theories: Prefix_Order, Sublist, and
    53   Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists.
    54 
    55 * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM
    56   New BNF-based (co)datatype package.
    57 
    58 * August 2012: Andrei Popescu and Dmitriy Traytel, TUM
    59   Theories of ordinals and cardinals.
    60 
    61 * July 2012: Makarius Wenzel, Université Paris-Sud / LRI
    62   Advanced support for Isabelle sessions and build management, notably
    63   "isabelle build".
    64 
    65 * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
    66   Simproc for rewriting set comprehensions into pointfree expressions.
    67 
    68 * May 2012: Andreas Lochbihler, KIT
    69   Theory of almost everywhere constant functions.
    70 
    71 * 2010-2012: Markus Kaiser and Lukas Bulwahn, TUM
    72   Graphview in Scala/Swing.
    73 
    74 
    75 Contributions to Isabelle2012
    76 -----------------------------
    77 
    78 * April 2012: Johannes Hölzl, TUM
    79   Probability: Introduced type to represent measures instead of
    80   locales.
    81 
    82 * April 2012: Johannes Hölzl, Fabian Immler, TUM
    83   Float: Moved to Dyadic rationals to represent floating point numers.
    84 
    85 * April 2012: Thomas Sewell, NICTA and
    86   2010: Sascha Boehme, TUM
    87   Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector
    88   equalities/inequalities.
    89 
    90 * March 2012: Christian Sternagel, JAIST
    91   Consolidated theory of relation composition.
    92 
    93 * March 2012: Nik Sultana, University of Cambridge
    94   HOL/TPTP parser and import facilities.
    95 
    96 * March 2012: Cezary Kaliszyk, University of Innsbruck and
    97   Alexander Krauss, QAware GmbH
    98   Faster and more scalable Import mechanism for HOL Light proofs.
    99 
   100 * January 2012: Florian Haftmann, TUM, et al.
   101   (Re-)Introduction of the "set" type constructor.
   102 
   103 * 2012: Ondrej Kuncar, TUM
   104   New package Lifting, various improvements and refinements to the
   105   Quotient package.
   106 
   107 * 2011/2012: Jasmin Blanchette, TUM
   108   Various improvements to Sledgehammer, notably: tighter integration
   109   with SPASS, support for more provers (Alt-Ergo, iProver,
   110   iProver-Eq).
   111 
   112 * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI
   113   Various refinements of local theory infrastructure.
   114   Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE.
   115 
   116 
   117 Contributions to Isabelle2011-1
   118 -------------------------------
   119 
   120 * September 2011: Peter Gammie
   121   Theory HOL/Library/Saturated: numbers with saturated arithmetic.
   122 
   123 * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
   124   Refined theory on complete lattices.
   125 
   126 * August 2011: Brian Huffman, Portland State University
   127   Miscellaneous cleanup of Complex_Main and Multivariate_Analysis.
   128 
   129 * June 2011: Brian Huffman, Portland State University
   130   Proof method "countable_datatype" for theory Library/Countable.
   131 
   132 * 2011: Jasmin Blanchette, TUM
   133   Various improvements to Sledgehammer, notably: use of sound
   134   translations, support for more provers (Waldmeister, LEO-II,
   135   Satallax). Further development of Nitpick and 'try' command.
   136 
   137 * 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
   138   Theory HOL/Library/Cset_Monad allows do notation for computable sets
   139   (cset) via the generic monad ad-hoc overloading facility.
   140 
   141 * 2011: Johannes Hölzl, Armin Heller, TUM and
   142   Bogdan Grechuk, University of Edinburgh
   143   Theory HOL/Library/Extended_Reals: real numbers extended with plus
   144   and minus infinity.
   145 
   146 * 2011: Makarius Wenzel, Université Paris-Sud / LRI
   147   Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
   148   Prover IDE.
   149 
   150 
   151 Contributions to Isabelle2011
   152 -----------------------------
   153 
   154 * January 2011: Stefan Berghofer, secunet Security Networks AG
   155   HOL-SPARK: an interactive prover back-end for SPARK.
   156 
   157 * October 2010: Bogdan Grechuk, University of Edinburgh
   158   Extended convex analysis in Multivariate Analysis.
   159 
   160 * October 2010: Dmitriy Traytel, TUM
   161   Coercive subtyping via subtype constraints.
   162 
   163 * October 2010: Alexander Krauss, TUM
   164   Command partial_function for function definitions based on complete
   165   partial orders in HOL.
   166 
   167 * September 2010: Florian Haftmann, TUM
   168   Refined concepts for evaluation, i.e., normalization of terms using
   169   different techniques.
   170 
   171 * September 2010: Florian Haftmann, TUM
   172   Code generation for Scala.
   173 
   174 * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
   175   Improved Probability theory in HOL.
   176 
   177 * July 2010: Florian Haftmann, TUM
   178   Reworking and extension of the Imperative HOL framework.
   179 
   180 * July 2010: Alexander Krauss, TUM and Christian Sternagel, University
   181     of Innsbruck
   182   Ad-hoc overloading. Generic do notation for monads.
   183 
   184 
   185 Contributions to Isabelle2009-2
   186 -------------------------------
   187 
   188 * 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM,
   189   Makarius Wenzel, TUM / LRI
   190   Elimination of type classes from proof terms.
   191 
   192 * April 2010: Florian Haftmann, TUM
   193   Reorganization of abstract algebra type classes.
   194 
   195 * April 2010: Florian Haftmann, TUM
   196   Code generation for data representations involving invariants;
   197   various collections avaiable in theories Fset, Dlist, RBT,
   198   Mapping and AssocList.
   199 
   200 * March 2010: Sascha Boehme, TUM
   201   Efficient SHA1 library for Poly/ML.
   202 
   203 * February 2010: Cezary Kaliszyk and Christian Urban, TUM
   204   Quotient type package for Isabelle/HOL.
   205 
   206 
   207 Contributions to Isabelle2009-1
   208 -------------------------------
   209 
   210 * November 2009, Brian Huffman, PSU
   211   New definitional domain package for HOLCF.
   212 
   213 * November 2009: Robert Himmelmann, TUM
   214   Derivation and Brouwer's fixpoint theorem in Multivariate Analysis.
   215 
   216 * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
   217   A tabled implementation of the reflexive transitive closure.
   218 
   219 * November 2009: Lukas Bulwahn, TUM
   220   Predicate Compiler: a compiler for inductive predicates to
   221   equational specifications.
   222 
   223 * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris
   224   HOL-Boogie: an interactive prover back-end for Boogie and VCC.
   225 
   226 * October 2009: Jasmin Blanchette, TUM
   227   Nitpick: yet another counterexample generator for Isabelle/HOL.
   228 
   229 * October 2009: Sascha Boehme, TUM
   230   Extension of SMT method: proof-reconstruction for the SMT solver Z3.
   231 
   232 * October 2009: Florian Haftmann, TUM
   233   Refinement of parts of the HOL datatype package.
   234 
   235 * October 2009: Florian Haftmann, TUM
   236   Generic term styles for term antiquotations.
   237 
   238 * September 2009: Thomas Sewell, NICTA
   239   More efficient HOL/record implementation.
   240 
   241 * September 2009: Sascha Boehme, TUM
   242   SMT method using external SMT solvers.
   243 
   244 * September 2009: Florian Haftmann, TUM
   245   Refinement of sets and lattices.
   246 
   247 * July 2009: Jeremy Avigad and Amine Chaieb
   248   New number theory.
   249 
   250 * July 2009: Philipp Meyer, TUM
   251   HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
   252   prover.
   253 
   254 * July 2009: Florian Haftmann, TUM
   255   New quickcheck implementation using new code generator.
   256 
   257 * July 2009: Florian Haftmann, TUM
   258   HOL/Library/Fset: an explicit type of sets; finite sets ready to use
   259   for code generation.
   260 
   261 * June 2009: Florian Haftmann, TUM
   262   HOL/Library/Tree: search trees implementing mappings, ready to use
   263   for code generation.
   264 
   265 * March 2009: Philipp Meyer, TUM
   266   Minimization tool for results from Sledgehammer.
   267 
   268 
   269 Contributions to Isabelle2009
   270 -----------------------------
   271 
   272 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
   273   Cambridge
   274   Elementary topology in Euclidean space.
   275 
   276 * March 2009: Johannes Hoelzl, TUM
   277   Method "approximation", which proves real valued inequalities by
   278   computation.
   279 
   280 * February 2009: Filip Maric, Univ. of Belgrade
   281   A Serbian theory.
   282 
   283 * February 2009: Jasmin Christian Blanchette, TUM
   284   Misc cleanup of HOL/refute.
   285 
   286 * February 2009: Timothy Bourke, NICTA
   287   New find_consts command.
   288 
   289 * February 2009: Timothy Bourke, NICTA
   290   "solves" criterion for find_theorems and auto_solve option
   291 
   292 * December 2008: Clemens Ballarin, TUM
   293   New locale implementation.
   294 
   295 * December 2008: Armin Heller, TUM and Alexander Krauss, TUM
   296   Method "sizechange" for advanced termination proofs.
   297 
   298 * November 2008: Timothy Bourke, NICTA
   299   Performance improvement (factor 50) for find_theorems.
   300 
   301 * 2008: Florian Haftmann, TUM
   302   Various extensions and restructurings in HOL, improvements
   303   in evaluation mechanisms, new module binding.ML for name bindings.
   304 
   305 * October 2008: Fabian Immler, TUM
   306   ATP manager for Sledgehammer, based on ML threads instead of Posix
   307   processes.  Additional ATP wrappers, including remote SystemOnTPTP
   308   services.
   309 
   310 * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen
   311   Prover for coherent logic.
   312 
   313 * August 2008: Fabian Immler, TUM
   314   Vampire wrapper script for remote SystemOnTPTP service.
   315 
   316 
   317 Contributions to Isabelle2008
   318 -----------------------------
   319 
   320 * 2007/2008:
   321   Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
   322   HOL library improvements.
   323 
   324 * 2007/2008: Brian Huffman, PSU
   325   HOLCF library improvements.
   326 
   327 * 2007/2008: Stefan Berghofer, TUM
   328   HOL-Nominal package improvements.
   329 
   330 * March 2008: Markus Reiter, TUM
   331   HOL/Library/RBT: red-black trees.
   332 
   333 * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and
   334   Lukas Bulwahn, TUM and John Matthews, Galois:
   335   HOL/Library/Imperative_HOL: Haskell-style imperative data structures
   336   for HOL.
   337 
   338 * December 2007: Norbert Schirmer, Uni Saarbruecken
   339   Misc improvements of record package in HOL.
   340 
   341 * December 2007: Florian Haftmann, TUM
   342   Overloading and class instantiation target.
   343 
   344 * December 2007: Florian Haftmann, TUM
   345   New version of primrec package for local theories.
   346 
   347 * December 2007: Alexander Krauss, TUM
   348   Method "induction_scheme" in HOL.
   349 
   350 * November 2007: Peter Lammich, Uni Muenster
   351   HOL-Lattice: some more lemmas.
   352 
   353 
   354 Contributions to Isabelle2007
   355 -----------------------------
   356 
   357 * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken
   358   State Spaces: The Locale Way (in HOL).
   359 
   360 * October 2007: Mark A. Hillebrand, DFKI
   361   Robust sub/superscripts in LaTeX document output.
   362 
   363 * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
   364     Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
   365   HOL-Word: a library for fixed-size machine words in Isabelle.
   366 
   367 * August 2007: Brian Huffman, PSU
   368   HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
   369 
   370 * June 2007: Amine Chaieb, TUM
   371   Semiring normalization and Groebner Bases.
   372   Support for dense linear orders.
   373 
   374 * June 2007: Joe Hurd, Oxford
   375   Metis theorem-prover.
   376 
   377 * 2007: Kong W. Susanto, Cambridge
   378   HOL: Metis prover integration.
   379 
   380 * 2007: Stefan Berghofer, TUM
   381   HOL: inductive predicates and sets.
   382 
   383 * 2007: Norbert Schirmer, TUM
   384   HOL/record: misc improvements.
   385 
   386 * 2006/2007: Alexander Krauss, TUM
   387   HOL: function package and related theories on termination.
   388 
   389 * 2006/2007: Florian Haftmann, TUM
   390   Pure: generic code generator framework.
   391   Pure: class package.
   392   HOL: theory reorganization, code generator setup.
   393 
   394 * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and
   395     Julien Narboux, TUM
   396   HOL/Nominal package and related tools.
   397 
   398 * November 2006: Lukas Bulwahn, TUM
   399   HOL: method "lexicographic_order" for function package.
   400 
   401 * October 2006: Stefan Hohe, TUM
   402   HOL-Algebra: ideals and quotients over rings.
   403 
   404 * August 2006: Amine Chaieb, TUM
   405   Experimental support for generic reflection and reification in HOL.
   406 
   407 * July 2006: Rafal Kolanski, NICTA
   408   Hex (0xFF) and binary (0b1011) numerals.
   409 
   410 * May 2006: Klaus Aehlig, LMU
   411   Command 'normal_form': normalization by evaluation.
   412 
   413 * May 2006: Amine Chaieb, TUM
   414   HOL-Complex: Ferrante and Rackoff Algorithm for linear real
   415   arithmetic.
   416 
   417 * February 2006: Benjamin Porter, NICTA
   418   HOL and HOL-Complex: generalised mean value theorem, continuum is
   419   not denumerable, harmonic and arithmetic series, and denumerability
   420   of rationals.
   421 
   422 * October 2005: Martin Wildmoser, TUM
   423   Sketch for Isar 'guess' element.
   424 
   425 
   426 Contributions to Isabelle2005
   427 -----------------------------
   428 
   429 * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
   430   HOL-Complex: Formalization of Taylor series.
   431 
   432 * September 2005: Stephan Merz, Alwen Tiu, QSL Loria
   433   Components for SAT solver method using zChaff.
   434 
   435 * September 2005: Ning Zhang and Christian Urban, LMU Munich
   436   A Chinese theory.
   437 
   438 * September 2005: Bernhard Haeupler, TUM
   439   Method comm_ring for proving equalities in commutative rings.
   440 
   441 * July/August 2005: Jeremy Avigad, Carnegie Mellon University
   442   Various improvements of the HOL and HOL-Complex library.
   443 
   444 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
   445   Some structured proofs about completeness of real numbers.
   446 
   447 * May 2005: Rafal Kolanski and Gerwin Klein, NICTA
   448   Improved retrieval of facts from theory/proof context.
   449 
   450 * February 2005: Lucas Dixon, University of Edinburgh
   451   Improved subst method.
   452 
   453 * 2005: Brian Huffman, OGI
   454   Various improvements of HOLCF.
   455   Some improvements of the HOL-Complex library.
   456 
   457 * 2005: Claire Quigley and Jia Meng, University of Cambridge
   458   Some support for asynchronous communication with external provers
   459   (experimental).
   460 
   461 * 2005: Florian Haftmann, TUM
   462   Contributions to document 'sugar'.
   463   Various ML combinators, notably linear functional transformations.
   464   Some cleanup of ML legacy.
   465   Additional antiquotations.
   466   Improved Isabelle web site.
   467 
   468 * 2004/2005: David Aspinall, University of Edinburgh
   469   Various elements of XML and PGIP based communication with user
   470   interfaces (experimental).
   471 
   472 * 2004/2005: Gerwin Klein, NICTA
   473   Contributions to document 'sugar'.
   474   Improved Isabelle web site.
   475   Improved HTML presentation of theories.
   476 
   477 * 2004/2005: Clemens Ballarin, TUM
   478   Provers: tools for transitive relations and quasi orders.
   479   Improved version of locales, notably interpretation of locales.
   480   Improved version of HOL-Algebra.
   481 
   482 * 2004/2005: Amine Chaieb, TUM
   483   Improved version of HOL presburger method.
   484 
   485 * 2004/2005: Steven Obua, TUM
   486   Improved version of HOL/Import, support for HOL-Light.
   487   Improved version of HOL-Complex-Matrix.
   488   Pure/defs: more sophisticated checks on well-formedness of overloading.
   489   Pure/Tools: an experimental evaluator for lambda terms.
   490 
   491 * 2004/2005: Norbert Schirmer, TUM
   492   Contributions to document 'sugar'.
   493   Improved version of HOL/record.
   494 
   495 * 2004/2005: Sebastian Skalberg, TUM
   496   Improved version of HOL/Import.
   497   Some internal ML reorganizations.
   498 
   499 * 2004/2005: Tjark Weber, TUM
   500   SAT solver method using zChaff.
   501   Improved version of HOL/refute.