Coq Formalisation of "Around Classical and Intuitionistic Linear Logics"

This is a partial formalisation of the work presented in the paper Around Classical and Intuitionistic Linear Logics (LICS'18).

It is based on the YALLA library for the Coq proof assistant.

For any question: olivier.laurent@ens-lyon.fr