Rocoma

This is a Rocq formalisation of The Logic of Recipes, from “Coma, an Intermediate Verification Language with Explicit Abstraction Barriers (extended version)” by Andrei Paskevich, Paul Patault and Jean-Christophe Filliâtre.

Project sources are available on Codeberg.

Main results

The reader may go directly to Table of content or else some selected theorems are listed bellow:

• confluence
• subject_reduction
• strong_normalization
• neutralization_soundness

Build instructions

Development

make

Documentation

The documentation built by coqdoc and pandoc can be found at the following link rocoma.paulpatault.fr/.

git clone https://github.com/rocq-community/coqdocjs/tree/master
ln -s coqdocjs/Makefile.doc Makefile.coq.local
make doc

Requirements

Installing these components via opam will allow you to install the required version of Rocq and all its sub-dependencies.

# install `opam`
bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)"
opam init

# setup a switch
opam switch create rocoma 5.3.0 --yes
opam switch rocoma --yes

# install packages
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-autosubst.1.9 coq-mathcomp-ssreflect.2.4.0 coq-mathcomp-zify.1.5.0+2.0+8.16 --yes

Licence

Files in the directory autosubst_lib are not mine but are copied from the Autosubst gallery.