blob: b4d808c961f601473acb95475e1f8344fc81af81 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
#+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~
- [X] Theorem 4.5 :: throughout ~Cfe.Derivation.Properties~
- [ ] Theorem 4.6 ::
- [ ] Theorem 4.7 ::
|
