diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2024-01-23 13:22:45 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2024-01-23 13:22:45 +0000 |
| commit | 06423f2a738b6ff94429ab84b4dcd3b443fd84bd (patch) | |
| tree | 010b96529f400c1289cc13ffef77fbd48170a454 /README.org | |
| parent | 848607d2e2579d127e7e9a723b9cfea14c2ce8c1 (diff) | |
Add a README detailing progress.
Diffstat (limited to 'README.org')
| -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 :: |