Coq Formalization of "Around Classical and Intuitionistic Linear Logics"

This is a partial formalization 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.

• self-contained original formalization based on an updated version (for Coq 8.7.1) of YALLA 1.0
  (open README.txt for more informations)