A Rocq formalisation of The Logic of Recipes, section 3 of “Coma, an Intermediate Verification Language with Explicit Abstraction Barriers” (Andrei Paskevich, Paul Patault, Jean-Christophe Filliâtre, TOPLAS 48(3), 2026; extended version on HAL).
Sources: codeberg.org/paulpatault/rocoma. Documentation: table of contents.
Recipes are the intermediate language of Coma: a λ-calculus with
continuations, assertions and the two constants 0 (failure)
and ⊤ (success). Section 3 of the paper gives them a logic:
a recipe is interpreted as a formula, two recipes are compared by
entailment, and the main results say how this logic behaves under
neutralisation, fusion, and against the joker recipes that bound
everything.
Everything from 3.1 to 3.11 is proved. The only assumptions are functional extensionality and the rules of the validity judgement on formulas, which are stated once as a module signature and proved in a semantic model. Lemma 3.12 (factorisation) is not done.
| paper | Rocq |
|---|---|
| Lemma 3.1, logical relations | logical_relation_lemma |
Theorem 3.2, ⟦ ⟧ is defined on complete recipes |
eval_def |
| Lemma 3.3, a neutralised recipe is neutral | neuneug |
| Lemmas 3.4 and 3.5, entailment is a preorder | entails_refl,
entails_trans |
| Lemma 3.6, pointwise entailment | entails_36 |
| Lemma 3.7, a fusion is a meet | fusion_meet |
| Corollaries 3.8 and 3.9 | cross_lemma,
entails_neu |
| Lemma 3.10, characterisation of meets | l_3_10 |
| Lemma D.1, every recipe submits to every signature | d1 |
| Theorem 3.11, jokers | joker_entails |
Recipes: syntax,
substitutions (with Autosubst), neutralisation, weight, depth, order of
a signature.Recipes_typing:
the typing judgement with forbidden windows, and its stability
lemmas.Recipes_stacks:
stacks of arguments and application chains s ∘ l.Recipes_eval:
evaluation of complete recipes into formulas, existence and
uniqueness.Recipes_evalf: a
functional evaluator with fuel, sound and complete for the relational
one; extracted to OCaml in Extraction.Recipes_logrel,
Recipes_box_rel,
Recipes_directly_box:
the logical relations and the induction scheme over boxed subrecipes
used by 3.3, 3.7 and D.1.Recipes_valid_sig:
the rules on valid, as a module type; Recipes_valid_model:
a model of them, where formulas are interpreted in
Prop.Recipes_neuneu:
neutrality and entailment, 3.3 to 3.6.Recipes_fusion:
fusion and meet, 3.7 to 3.10.Recipes_joker:
the joker recipes of Fig. 6, the cover and submit relations of Appendix
D, Lemma D.1 and Theorem 3.11.Variables are de Bruijn indices, in both sorts (recipes and terms). This has two visible consequences.
The clause of the logical relation for a functional signature asks the argument to be related under every renaming of its term variables, not only as it stands: without this the relation is not stable under the renamings that appear when a proof goes under a term binder. Corollaries 3.10.3 and 3.10.4 inherit this extra hypothesis.
The cover relation of Appendix D carries a counter of the term
binders crossed: a box placed under k binders contains the
recipe of the stack shifted by k, which the paper does not
need to say.
Two rules on valid are added to the ones the paper uses,
the two quantifier rules in de Bruijn form (introduction with a shifted
context, elimination by substitution). They hold in the model.
Files in autosubst_lib are copied from the Autosubst
gallery.