The paper makes the following mechanization claims:
- Theorem 6.4 claims that forward-completeness suffices for
associativity of evidence composition and that there exists a
generalized Coq mechanization of this property.
This section has been mechanized in file agt/AGT_Spec.v:
- Definition 6.1 (forward completeness) corresponds to
Parameter gamma_completeness. - Theorem 6.4 (associativity of evidence composition) corresponds
to
Theorem ct_assoc.
- Definition 6.1 (forward completeness) corresponds to
- Theorem 7.4 claims a bound for the size of evidence composition
in the BRR language. The height bounds in Lemma 7.3 and Theorem
7.4 are proven in Coq.
This section has been mechanized in file agt/space_efficiency_in_brr.v
- Lemma 7.1 (Bound for size of Gradual Types in BRR)
corresponds to
Lemma height_bound. - Definition 7.2 (Size and height of evidences in BRR)
has three parts:
- Part 1 (size of evidences) corresponds to
Definition size_ev. - Part 2 (height of evidences) corresponds to
Definition height_ev. - Part 3 (label domain of evidences) corresponds to
Definition domain_ev.
- Part 1 (size of evidences) corresponds to
- Theorem 7.3 (Height bounds in BRR) has three parts:
- Part 1 (bound for meet) corresponds to
Lemma height_meet. - Part 2 (bound for initial evidence) corresponds to
Lemma I_bound. - Part 3 (bound for composition) corresponds to
Lemma ec_bound_height.
- Part 1 (bound for meet) corresponds to
- Theorem 7.4 corresponds to
Theorem ec_bound_size.
- Lemma 7.1 (Bound for size of Gradual Types in BRR)
corresponds to
An interpreter for the gradual rows language as presented in the paper.
Interpreter for RL with modified evidences. This interpreter is not space efficient.
Interpreter for RL+ with Bounded Records and Rows (BRR) This interpreter is space efficient.