YALLA: an LL library for Coq
Yet Another deep embedding of Linear Logic in Coq
This library for Coq defines a
generic predicate for provability in various fragments
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.
- explicit exchange rule (for full or cyclic exchange)
- parametrized use of mix, mix0, axioms, etc.
- cut elimination, sub-formula property, deduction theorem, etc.
- relations with ILL
- interfaces for multi-set based systems, Lambek calculus, etc.
- current public release: yalla 1.0 (2017/07/18)
- available in working branch:
- move to Coq 8.8.0
- generalized conservativity results for LL over ILL
- variants: polarized linear logic, tensor logic
- general move from
- also planned for next release:
- LL cut elimination deduced from cut elimination for full ILL (ongoing)
- cut elimination for full ILL
- on demand...
- future work:
- parametric exponential rules
For any question, trouble, feature request, help needed, contributions, etc: firstname.lastname@example.org