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 > Makefile
and compile by calling
WARNING : 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.
WORK WITH THE CODE
Call coqide as follows from the root of the library:
$ coqide -R . CatSem
Read 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.