Skip to content
Formalization of Linear Logic in Coq
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

Propositional and First Order Linear Logic in Coq

We formalize in Coq different sequent calculi for propositional and first order linear logic (LL) and we prove them to be equivalent. We also prove some meta-theorems, including cut-elimination and the completeness of the focused system. The focused system can be then used for proving adequacy between LL and (logical / computational) systems encoded in LL. See for instance the example in ./FOLL/Examples/LJLL.v

This package is free software; you can redistribute it and/or modify it under the terms of GNU Lesser General Public License (see the COPYING file).

Author Bruno Xavier and Carlos Olarte

Getting Started

The project was tested in Coq 8.7. No extra library is needed for compilation.

There are two main directories

  • PLL : Formalizing propositional linear logic.
  • FOLL : Formalizing first order linear logic.

In both directories, the source files can be compiles with


and HTML documentation can be generated with

make html
You can’t perform that action at this time.