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)
- planned for next release:
- move to Coq 8.7.1 (done, ask if needed)
- focusing (done, ask if needed)
- generalized conservativity results for LL over ILL (done, ask if needed)
- cut elimination for full ILL (ongoing)
- variants: polarized linear logic, tensor logic (done, ask if needed)
- on demand...
For any question, trouble, feature request, help needed, contributions, etc: firstname.lastname@example.org