nLab system L

Idea

The term “system L” may refer to (at least) two different concepts in formal logic:

• there is a syntax for sequent calculus introduced in (Curien-Herbelin 00) under the name $\lambda \bar \mu \mu$-calculus, whose name then changed in time to “system L” in reference to the “L” in “LK”, “LJ”, from Gerhard Gentzen‘s original terminology of sequent calculi;

• there is a natural deduction system of this name, see System L.

References

The sequent calculus

• Pierre-Louis Curien, Hugo Herbelin, The duality of computation, Proceeding ICFP ‘00 Proceedings of the fifth ACM SIGPLAN international conference on Functional programming Pages 233 - 243 (web)

• Arnaud Spiwack, section 5 of A dissection of L, preprint pdf

The natural deduction system

• Wikipedia, System L