YALLA: an LL library for Coq
Yet Another deep embedding of Linear Logic in Coq
This library for Coq defines a
generic notions of proofs for various fragments
logic. It provides some general results such as cut admissibility,
The formalisation is based on sequents as lists together with an
explicit exchange rule, as well as proof objects in
Type. This allows us to provide a study of proofs
which is compatible with the computational interpretation of proofs.
- explicit exchange rule (for full or cyclic exchange)
- parametrized use of mix, mix0, axioms, etc.
- cut admissibility, sub-formula property, deduction theorem, etc.
- relations with ILL
- interfaces for multi-set based systems, Lambek calculus, etc.
- first public release: yalla 1.0 (2017/07/18)
- current public release: yalla 2.0 (2019/01/23)
- move to Coq 8.9.0
- general move from
- cut admissibility for full ILL
- generalized conservativity results for LL over ILL
- variants: polarized linear logic, tensor logic
- available in working branch
- ongoing work:
- primitive permutations
- phase semantics
- future work:
- parametric exponential rules
- denotational semantics
- on demand...
For any question, trouble, feature request, help needed, contributions, etc: firstname.lastname@example.org