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

• Opam-based installation procedure (for v2.0.4)

  
      $ opam repo add coq-released https://coq.inria.fr/opam/released
      $ opam install coq-yalla	
      

• Manual installation procedure (all versions)
  0. (install OLlibs if you want to use the working branch)
  1. download and unpack the files for v2.0.4 (or for the working branch)
  2. move into the created directory and run:

     
     $ ./configure
     $ make
     $ make install
           

Releases

• 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)
  • move to Coq 8.12.0
  • the internal version of OLlibs matches OLlibs 2.0.0
• yalla 2.0.2 (2021/01/13)
  • move to Coq 8.13.0 (compatible with Coq 8.14 as well)
  • the internal version of OLlibs matches OLlibs 2.0.1
• yalla 2.0.3 (2022/02/06)
  • move to Coq 8.15
  • the internal version of OLlibs matches OLlibs 2.0.2
• current public release: yalla 2.0.4 (2023/04/09)
  • move to Coq 8.17 (compatible with Coq 8.16 as well)
  • the internal version of OLlibs matches OLlibs 2.0.4
• available in working branch
  • move to Coq 8.17
  • rely on external standard library extension OLlibs release 2.0.4
  • generalized mix rules
  • generalized parameter for cut-rules on a formula basis
  • more on focusing
• ongoing work:
  • primitive permutations
  • phase semantics
  • parametric exponential rules
  • denotational semantics
  • proof nets
• future work:
  • quantifiers
  • on demand...

Documents

• ReadMe
• Preliminary Report (Coq Workshop 2018)
• Talk at Linearity - TLLA 2020

Contact