#+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 ::