YALLA : an LL library for Coq
=============================
Yet Another deep embedding of Linear Logic in Coq
[If you have any trouble, question or request for extension,
if you need help to write interfaces,
please contact the author: *** Olivier.Laurent@ens-lyon.fr *** ]
This library defines a generic predicate for provability in various
fragments of linear logic. It provides some general results such as
cut-elimination.
The formalisation is based on sequents as lists together with an
explicit exchange rule. This allows us to provide a study of proofs
which is compatible with the computational interpretation of proofs.
Parameters allow the user:
- to include the mix0 rule or not;
- to include the mix2 rule or not;
- to define arbitrary axioms
(which allows in particular to work with open proofs);
- to use the usual exchange rule (arbitrary permutations);
or to restrict to cyclic linear logic (cyclic permutations only).
This library is not appropriate to build LL proofs by hands, but more
for the study of meta-properties of linear logic fragments.
Because of the parameters, the proof predicates defined in the library
should not be used directly. We recommend the user to define his own
objects (inductives for formulas and proofs) and to interface them
with the library in order to then import the results of the library in
his lighter setting (examples of such interfaces are provided in the
files mell2.v and lambek.v).
Main files:
- formulas.v(o)
definition of linear logic formulas
- fmformulas.v(o)
additional structure on formulas (order, multiset)
- ll.v(o)
main library for classical linear logic (LL)
- iformulas.v(o)
definition of intuitionistic linear logic formulas
- fmiformulas.v(o)
additional structure on intuitionistic formulas (order, multiset)
- ill.v(o)
intuitionistic linear logic (ILL)
(Lambek calculus included when permutation is equality:
ipperm P = false)
- subs.v(o)
susbtitution for LL
- ll_fragments.v(o)
definitions of some common fragments of LL
Example files for interfaces:
- mell2.v(o)
unit-free MELL with mix2
- lambek.v(o)
a variant of Lambek calculus
- mell_mset.v(o)
multiset-based MELL (no exchange rule)
- mell_msetoid.v(o)
setoid multiset-based MELL
- llpol.v(o)
polarized fragment of LL
Other files:
- bbb.v(o)
study of LL extended with the equation: bot = oc bot
- nn.v(o)
properties of double-negation translations from LL to ILL