Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Intuitionistic Sequent-Style Calculus with Explicit Structural Rules
verfasst von : Silvia Ghilezan, Jelena Ivetić, Pierre Lescanne, Dragisa Žunić
Erschienen in: Logic, Language, and Computation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper we extend the Curry-Howard correspondence to intuitionistic sequent calculus with explicit structural rules of weakening and contraction. We present a linear term calculus derived from the calculus of Espírito Santo, which captures the computational content of the intuitionistic sequent logic, by adding explicit operators for weakening and contraction. For the proposed calculus we introduce the type assignment system with simple types and prove some operational properties, including the subject reduction and strong normalisation property. We then relate the proposed linear type calculus to the simply typed intuitionistic calculus of Kesner and Lengrand, which handles explicit operators of weakening and contraction in the natural deduction framework.