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:

See more.





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