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.
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, A dissection of L (2014) [pdf]
Last revised on August 21, 2023 at 08:35:25. See the history of this page for a list of all contributions to it.