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