Formalization

This release consists on the formalization of propositional and first-order (using PHOAS) linear logic in Coq, plus a small example specification of LJ. It is described in the paper:

"Mechanizing Linear Logic in Coq". Bruno Xavier, Carlos Olarte, Giselle Reis and Vivek Nigam, LSFA 2017.