From 7b6a32fe1ebc0a0a1b22fd3a0430c3c3e62992a7 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 9 Aug 2016 12:33:42 +0200 Subject: [PATCH] CHANGELOG: Update to account for newly introduced version 2.0-rc2 --- CHANGELOG.md | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 928f2ae5b..892ad8cc2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,26 +7,30 @@ Coq development, but not every API-breaking change is listed. Changes marked * [#] View shifts are radically simplified to just internalize frame-preserving updates. Weakestpre is defined inside the logic, and invariants and view - shifts with masks are also coded up inside Iris. + shifts with masks are also coded up inside Iris. Adequacy of weakestpre + is proven in the logic. * [#] The language can now fork off multiple threads at once. ## Iris 2.0 -This version accompanies the final ICFP paper. - -* [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] Due to a lack of maintenance and usefulness, lifting lemmas + for Hoare triples are removed. + +## Iris 2.0-rc2 + +This version matches the final ICFP paper. + +* [algebra] Make the core of an RA or CMRA a partial function. * [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 -- GitLab