Yalla

Yet Another deep embedding of Linear Logic in Rocq

Installation

Requires OLlibs v2.1.1 (add-ons for the standard library): see installation instructions.

1. install OLlibs v2.1.1

2. install Yalla

    $ ./configure
    $ make
    $ make install
   

Description

• microyalla: kernel version of yalla
• yalla: a deep embedding of variants of linear logic in Rocq

See the more detailed README for more informations.

See the release notes for versions history.

---

Main contributors

• Olivier Laurent
• Christophe Lucas

Many thanks also to Damien Pous and Christian Doczkal for important discussions, suggestions and help.