diff options
| -rw-r--r-- | README.org | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/README.org b/README.org new file mode 100644 index 0000000..666898e --- /dev/null +++ b/README.org @@ -0,0 +1,30 @@ +#+title: cfe-proof + +This Agda library is a verified implementation of [[https://doi.org/10.1145/3314221.3314625][A Typed, Algebraic Approach to +Parsing]]. + +* Proofs + +- [X] Proposition 3.1 :: throughout ~Cfe.Expression.Properties~ +- [X] Proposition 3.2 :: ~Cfe.Expression.Properties.⟦⟧-mono-env~ +- [X] Lemma 3.3 :: ~Cfe.Language.Properties.∪-selective~ +- [X] Lemma 3.4 :: ~Cfe.Language.Properties.∙-unique~ +- [ ] Lemma 3.5 :: throughout ~Cfe.Language.Properties~. In the paper, statement + 2 is false; a language satisfying \(\tau_\epsilon\) is at most \(\{\epsilon\}\). + - [X] 1 + - [X] 2 + - [X] 3 + - [X] 4 + - [X] 5 + - [ ] 6 + - [ ] 7 +- [X] Lemma 4.1 :: throughout ~Cfe.Judgement.Properties~ +- [X] Lemma 4.2 :: throughout ~Cfe.Judgement.Properties~ +- [X] Theorem 4.3 :: ~Cfe.Judgement.Properties.soundness~ +- [X] Lemma 4.4 :: ~Cfe.Judgement.Properties.subst₂-pres-rank~ +- [ ] Theorem 4.5 :: throughout ~Cfe.Derivation.Properties~ + - [X] Semantics to derivation + - [X] Derivation to semantics + - [ ] Uniqueness of derivation +- [ ] Theorem 4.6 :: +- [ ] Theorem 4.7 :: |