Skip to content

Formalization

Latest
Compare
Choose a tag to compare
@gisellemnr gisellemnr released this 03 Aug 08:53
· 35 commits to master since this release

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.