Home

Practice

C1ick ⅋ c⊗LLec⊥ tutorial

Linear Logic Tutorial

Examples

Cut Elimination

Enhancement Proposals

Roadmap

Testing Phase (available soon)

• extending special mode for proof transformations: reversing, focusing, etc.

Near Future

• add colors to follow occurrences

Other directions

• two-sided sequent calculus
• intuitionistic linear logic (click on a comma to apply right-hand side ⊗-rule)
• other linear logic variants (ELL, SLL, LLL, etc.)
• quantifiers (issue #16)
• contexts as first-class objects (issue #13)
• cyclic linear logic (exchange restricted to circular shifts, requires to modify the definition of dual of a formula)
• explicit exchange rule (with colored backgrounds to follow instances of formulas) (issue #11)
• back edges for regular proofs
• fixed-point connectives in formulas
• mix rules (note mix₂ can be faithfully simulated by adding ?(⊥⊗⊥) in the context, and similarly for mix₀ with ?1)
• export to proof-nets