Description of the Computer Aided Linear Logic project and its components
We aim at developing a family of tools for manipulating linear logic (proofs) on a computer. These tools should be able to interact in order to provide the richest possible linear logic environment. This relies on some common representations of formulas, proofs, etc.
Here are some examples of such interactions:
categories: interactive prover / graphical interface
Web-based interactive theorem prover for linear logic. It includes some automated features, export to NanoYalla kernel and other formats, proof transformations (cut elimination, axiom expansion, etc.).
categories: tool / interface
Keypad configuration files to get direct access to UTF-8 linear-logic-related symbols.
categories: formalization, kernel
Kernel formalization of propositional Linear Logic in Coq.
categories: formalization
Coq formalization (deep embedding) of Linear Logic.
It includes part of NanoYalla.
Natural candidates for integration in the CALL framework
categories: benchmark
Collection of classical and intuitionistic linear logic formulas to be used as a benchmark for provers.
categories: automated prover
A focused automated theorem prover for linear logic.
categories: automated prover
A focused automated theorem prover for linear logic.
categories: automated prover
A focused automated theorem prover for linear logic.
categories: interactive prover
Interactive proof construction by linking.