Repository containing the formalisation that goes with our draft entitled "Encode the Cake and Eat it Too: Controlling computation in type theory, locally".
See the rendered Rocq code, with comments.
You need the Rocq prover 9.0, Equations and Autosubst 2 OCaml (needs ocaml<5, recommended 4.14.2). You can install them using
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install --deps-only .Then to verify the proof, just use make:
make autosubst
make