YALLA: an LL library for Coq
Yet Another deep embedding of Linear Logic in Coq
This library for Coq defines a
generic notion of proofs for various fragments
of linear
logic. It provides some general results such as cut admissibility,
etc.
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.
Some ingredients:
- explicit exchange rule (for full or cyclic exchange)
- parametrized use of mix rules, axioms, etc.
- cut admissibility, sub-formula property, deduction theorem, etc.
- relations with ILL
- interfaces for multi-set based systems, Lambek calculus, etc.
See more.
Installation
- first public release: yalla 1.0 (2017/07/18)
- yalla 2.0 (2019/01/23)
- move to Coq 8.9.0
- general move from
Prop
to Type
- cut admissibility for full ILL
- generalized conservativity results for LL over ILL
- focusing
- variants: polarized linear logic, tensor logic
- yalla 2.0.1 (2020/08/07)
- yalla 2.0.2 (2021/01/13)
- yalla 2.0.3 (2022/02/06)
- yalla 2.0.4 (2023/04/09)
- move to Coq 8.18 (compatible with Coq 8.16 and Coq 8.17 as well)
- the internal version of OLlibs matches OLlibs 2.0.4
- yalla 2.0.5 (2024/09/15)
- current public release: yalla 2.0.6 (2024/09/16)
- available in working branch
- move to Coq 8.20
- rely on external standard library extension OLlibs release 2.0.7
- generalized mix rules
- generalized parameter for cut-rules on a formula basis
- more on focusing (including Andreoli's triadic system)
- ongoing work:
- primitive permutations
- phase semantics
- parametric exponential rules
- denotational semantics
- proof nets
- future work:
- quantifiers
- implicit exchange rules
- on demand...
Documents
Contact
For any question, trouble, feature request, help needed, contributions, etc: olivier.laurent@ens-lyon.fr