Skip to content

Commit

Permalink
bump readme
Browse files Browse the repository at this point in the history
  • Loading branch information
co-dan committed Nov 13, 2023
1 parent ff5516c commit 25a2d60
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ approach of (Benton, Hur, Kennedy, McBride, JAR 2012) with well-scoped
terms and substitutions/renamings.


## Disjunction property
### Disjunction property
Some results in the formalization make use of the disjunction property
of Iris: if (P ∨ Q) is provable, then either P or Q are provable on
their own. This propery is used to show safety of the weakest
Expand All @@ -101,7 +101,7 @@ formalization, we added the disjunction propety as an assumption to
the safety theorem (`wp_safety`) and all of its instances (e.g. in
logical relations).

## Ground type of errors
### Ground type of errors

One other difference with the paper worth mentioning, is that in the
formalization we "hardcode" the type `Err` of errors, whereas in the
Expand Down

0 comments on commit 25a2d60

Please sign in to comment.