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.
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 .
- Pierre-Louis Curien and Guillaume Munch-Maccagnoni. The duality of computation under focus. 2010.