Linear Logic

Stream: general

[David Hanson]

Hello, I am new here so I apologize if this is not the correct place to ask this question. I was looking through some of the Mathlib documentation and trying to find out if linear logic has, at all, been implemented. If it has not, is this something that would be out of the scope of Mathlib, or is this just something that hasn't been undertaken by anyone, yet?

[Mario Carneiro]

It has not been implemented. The closest thing I can think of is https://github.com/leanprover-community/iris-lean, which implements a tactic mode for a separation logic with some substructural features (but isn't exactly classical linear logic)

[Schrodinger ZHU Yifan]

How about Lambek Calculus? I feel like doing some linguistic schoolwork in Lean. Do we have relevant formulation in lean such that I can look into?

[Dean Young]

@Schrodinger ZHU Yifan I like the idea of a simple experiment with binding order and two arrows like lambek/montague grammar.