# System L

**System L** is a family of syntax for a variety of variants of linear logic, inspired from classical calculi such as -calculus. These, in turn, stem from the study of abstract machines for λ-calculus. In this realm, polarization and focalization are features that appear naturally. Positives are typically values, and negatives pattern-matches. Contraction and weakening are implicit.

We present here a system for explicitely polarized and focalized linear logic. Polarization classifies terms and types between positive and negative; focalization separates values from non-values.

## Contents |

## Definitions

Positive types:

Negative types:

Positive values:

Positive terms:

Negative terms:

Commands:

## Typing

There are as many typing sequents classes as there are terms classes. Typing of positive values corresponds to focalized sequents, and commands are cuts.

Positive values: sequents are of the form .

Positive terms: sequents are of the form .

Negative terms: sequents are of the form .

Commands:

## Reduction rules

## References

- Pierre-Louis Curien and Guillaume Munch-Maccagnoni.
*The duality of computation under focus*. 2010.