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

• Coq/Rocq: version TODO
• Autosubst: version TODO

Licence

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