Phase Semantics

Some formalizations of linear logic in the Coq proof assistant.

Install

Using OPAM:

opam repo add coq-unstable https://github.com/coq/repo-unstable.git
opam install -j4 -v coq:phase-semantics

Compile from the sources

Install the AAC-Tactics library and run:

./configure.sh
make