CHANGELOG.md 1.54 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3
In this changelog, we document "large-ish" changes to Iris that affect even the
way the logic is used on paper.  We also mention some significant changes in the
Coq development, but not every API-breaking change is listed.  Changes marked
4 5 6 7 8 9 10 11
[#] still need to be ported to the Iris Documentation LaTeX file(s).

## Iris 3.0

* [#] 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.
* [#] The language can now fork off multiple threads at once.
Ralf Jung's avatar
Ralf Jung committed
12 13 14

## Iris 2.0

Ralf Jung's avatar
Ralf Jung committed
15 16
This version accompanies the final ICFP paper.

Ralf Jung's avatar
Ralf Jung committed
17
* [algebra] Make the core of an RA or CMRA a partial function.
Ralf Jung's avatar
Ralf Jung committed
18 19 20 21
* [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.
22 23
* [program_logic/language] The language does not define its own "atomic"
  predicate.  Instead, atomicity is defined as reducing in one step to a value.
Ralf Jung's avatar
Ralf Jung committed
24
* [program_logic/lifting] Lifting lemmas no longer round-trip through a
Ralf Jung's avatar
Ralf Jung committed
25 26 27 28 29
  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.
Ralf Jung's avatar
Ralf Jung committed
30 31 32 33

## Iris 2.0-rc1

This is the Coq development and Iris Documentation as submitted to ICFP.