The 𝜆𝜇𝜇˜-calculus is a well-established variant used for term assignment in the sequent calculus, which differs from natural deduction. The sequent calculus, first introduced by Gentzen, operates using sequents that involve multiple formulas and contexts. Notation in the 𝜆𝜇𝜇˜-calculus, notably from Curien and Herbelin, emphasizes this correspondence yet can complicate rule articulation when extending language features. Recommended readings for deeper understanding include works by Negri, Von Plato, Troelstra, and Schwichtenberg.
The original article which introduced the 𝜆𝜇𝜇˜-calculus as a term assignment system for the sequent calculus was by Curien and Herbelin [2000].
The notation of Curien and Herbelin [2000] with its two contexts Γ and Δ perfectly illustrates the correspondence to the sequent calculus which operates with sequents Γ ⊢ Δ.
For a more thorough introduction to the sequent calculus as a logical system, we can recommend the books by Negri and Von Plato [2001] and Troelstra and Schwichtenberg [2000].
The sequent calculus was originally introduced by Gentzen in the articles Gentzen [1935a,b, 1969].
Collection
[
|
...
]