From 25a2d60c13d28812051d2bad922ecc9cd2d1909b Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Mon, 13 Nov 2023 10:40:31 +0100 Subject: [PATCH] bump readme --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 7410271..865ab57 100644 --- a/README.md +++ b/README.md @@ -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 @@ -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