CHANGELOG.md 799 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4
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
[#] still need to be ported to the Iris Documentation LaTeX file.
Ralf Jung's avatar
Ralf Jung committed
5 6 7

## Iris 2.0

Ralf Jung's avatar
Ralf Jung committed
8 9 10 11 12 13 14
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.
Ralf Jung's avatar
Ralf Jung committed
15 16 17 18

## Iris 2.0-rc1

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