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 of linear logic. It provides some general results such as cut-elimination, etc.

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.

Some ingredients:

See more.




For any question, trouble, feature request, help needed, contributions, etc: olivier.laurent@ens-lyon.fr