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, section 5 of A dissection of L, preprint pdf
Last revised on May 5, 2014 at 04:16:45. See the history of this page for a list of all contributions to it.