Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joshua Yanovski
iris-coq
Commits
7b6a32fe
Commit
7b6a32fe
authored
Aug 09, 2016
by
Ralf Jung
Browse files
CHANGELOG: Update to account for newly introduced version 2.0-rc2
parent
53325866
Changes
1
Hide whitespace changes
Inline
Side-by-side
CHANGELOG.md
View file @
7b6a32fe
...
@@ -7,26 +7,30 @@ Coq development, but not every API-breaking change is listed. Changes marked
...
@@ -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
*
[#] View shifts are radically simplified to just internalize frame-preserving
updates. Weakestpre is defined inside the logic, and invariants and view
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.
*
[#] The language can now fork off multiple threads at once.
## Iris 2.0
## 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
*
[heap_lang] No longer use dependent types for expressions. Instead, values
carry a proof of closedness. Substitution, closedness and value-ness proofs
carry a proof of closedness. Substitution, closedness and value-ness proofs
are performed by computation after reflecting into a term langauge that knows
are performed by computation after reflecting into a term langauge that knows
about values and closed expressions.
about values and closed expressions.
*
[program_logic/language] The language does not define its own "atomic"
*
[program_logic/language] The language does not define its own "atomic"
predicate. Instead, atomicity is defined as reducing in one step to a value.
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
*
[program_logic/lifting] Lifting lemmas no longer round-trip through a
user-chosen predicate to define the configurations we can reduce to; they
user-chosen predicate to define the configurations we can reduce to; they
directly relate to the operational semantics. This is equivalent and
directly relate to the operational semantics. This is equivalent and
much simpler to read.
much simpler to read.
Due to a lack of maintenance and usefulness, lifting lemmas for Hoare triples
are removed.
## Iris 2.0-rc1
## Iris 2.0-rc1
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment