NEWS and CONTRIBUTORS for 8b50f29a1992
authorAndreas Lochbihler
Thu May 17 07:42:33 2018 +0200 (5 days ago)
changeset 682005859c688102a
parent 68199 f551dd2178ab
child 68201 dee993b88a7b
NEWS and CONTRIBUTORS for 8b50f29a1992
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Wed May 16 23:13:33 2018 +0200
     1.2 +++ b/CONTRIBUTORS	Thu May 17 07:42:33 2018 +0200
     1.3 @@ -14,6 +14,10 @@
     1.4  * May 2018: Florian Haftmann
     1.5    Consolidation of string-like types in HOL.
     1.6  
     1.7 +* May 2018: Andreas Lochbihler (Digital Asset),
     1.8 +  Pascal Stoop (ETH Zurich)
     1.9 +  Code generation with lazy evaluation semantics.
    1.10 +
    1.11  * March 2018: Florian Haftmann
    1.12    Abstract bit operations push_bit, take_bit, drop_bit, alongside
    1.13    with an algebraic foundation for bit strings and word types in
     2.1 --- a/NEWS	Wed May 16 23:13:33 2018 +0200
     2.2 +++ b/NEWS	Thu May 17 07:42:33 2018 +0200
     2.3 @@ -262,6 +262,11 @@
     2.4  parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
     2.5  some examples.
     2.6  
     2.7 +* A new preprocessor for the code generator to generate code for algebraic
     2.8 +  types with lazy evaluation semantics even in call-by-value target languages.
     2.9 +  See theory HOL-Library.Code_Lazy for the implementation and
    2.10 +  HOL-Codegenerator_Test.Code_Lazy_Test for examples.
    2.11 +
    2.12  * SMT module:
    2.13    - The 'smt_oracle' option is now necessary when using the 'smt' method
    2.14      with a solver other than Z3. INCOMPATIBILITY.