Forked from
Iris / Iris
6353 commits behind the upstream repository.
CHANGELOG.md 799 B
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.
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.
Iris 2.0-rc1
This is the Coq development and Iris Documentation as submitted to ICFP.