This Coq theory compiles under Coq 8.3pl5, available from https://coq.inria.fr/distrib/V8.3pl5/files/ . Earlier patch levels should also work; I have tested with 8.3pl2.
Create a Makefile by calling
$ coq_makefile -f Make > Makefileand compile by calling
$ makeWARNING : The compilation of some of the files consumes up to 2GB of memory. Make sure you dispose of sufficient reserves of ram before compiling the code.
Call coqide as follows from the root of the library:
$ coqide -R . CatSemRead the file "./DESCRIPTION" for a description of the content of each file.
Each branch below, printed in boldface, corresponds to an article, printed in italic.
- JFR: Initial Semantics for higher-order typed syntax in Coq
- MSCS: Modules over relative monads for syntax and semantics
- REDUCTION_RULES: Initial Semantics for Reduction Rules
All the articles are also available from my webpage.