Commit 7453c926 authored by Ralf Jung's avatar Ralf Jung
Browse files

add missing item to CHANGELOG

parent 5d8b2eb6
......@@ -7,13 +7,19 @@ Coq development, but not every API-breaking change is listed. Changes marked
This version accompanies the final ICFP paper.
* [# algebra] Make the core of an RA or CMRA a partial function.
* [algebra] Make the core of an RA or CMRA a partial function.
* [heap_lang] No longer use dependent types for expressions. Instead, values
carry a proof of closedness. Substitution, closedness and value-ness proofs
are performed by computation after reflecting into a term langauge that knows
about values and closed expressions.
* [program_logic/language] The language does not define its own "atomic"
predicate. Instead, atomicity is defined as reducing in one step to a value.
* [# program_logic/lifting] Lifting lemmas no longer round-trip through a
user-chosen predicate to define the configurations we can reduce to; they
directly relate to the operational semantics. This is equivalent and
much simpler to read.
Due to a lack of maintenance and usefulness, lifting lemmas for Hoare triples
are removed.
## Iris 2.0-rc1
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment