Rocq formalisation of section 3 (The Logic of Recipes) of the Coma paper, TOPLAS 48(3), 2026, by Andrei Paskevich, Paul Patault and Jean-Christophe Filliâtre. There is an extended version on HAL.
Code on codeberg, coqdoc here.
Everything from 3.1 to 3.11 is proved.
Axioms: functional extensionality, and the rules on
valid. These rules are a module type (Recipes_valid_sig)
and have a model in Prop (Recipes_valid_model).
Main prints the
definitions, the statements and the axioms they use.
| paper | Rocq |
|---|---|
| 3.1 | logical_relation_lemma |
| 3.2, ⟦ ⟧ is defined on complete recipes | eval_def |
| 3.3 | neuneug |
| 3.4, 3.5 | entails_refl,
entails_trans |
| 3.6 | entails_36 |
| 3.7, fusion is a meet | fusion_meet |
| 3.8, 3.9 | cross_lemma,
entails_neu |
| 3.10 | l_3_10 |
| D.1 | d1 |
| 3.11, jokers | joker_entails |
In dependency order, roughly:
Recipes: syntax
(with Autosubst), neu, weight, depth, orderRecipes_typingRecipes_stacks:
s ∘ lRecipes_logrel,
Recipes_directly_box,
Recipes_box_rel:
logical relations, and the induction on boxed subrecipesRecipes_eval: ⟦ ·
⟧, existence and uniquenessRecipes_evalf:
evaluation with fuel, extracted to OCaml (in file Extraction)Recipes_neuneu:
3.3 to 3.6Recipes_fusion:
3.7 to 3.10Recipes_joker:
jokers, appendix D, lemma 3.11We use de Bruijn indices for both recipes and terms.
For a functional signature, the logical relation asks the argument to be related under every renaming of its term variables.
The cover relation of appendix D counts the term binders crossed:
under k binders, a box contains the recipe of the stack
shifted by k. The paper does not have to say it
explicitely.
We also need the two quantifier rules on valid in de
Bruijn form.
autosubst_lib is copied from the Autosubst
gallery.
I used Claude (Anthropic) to help write this website and the README.