Intuitionistic Sequent-Style Calculus with Explicit Structural Rules

Pierre Lescanne; Silvia Ghilezan; Jelena Ivetic; Dragisa Zunic

Intuitionistic Sequent-Style Calculus with Explicit Structural Rules

Pierre Lescanne ¹ Silvia Ghilezan ² Jelena Ivetic ² Dragisa Zunic

1 LIP - Laboratoire de l'Informatique du Parallélisme

2 Faculty of engineering, University of Novi Sad

Abstract : In this paper we extend the Curry-Howard correspondence to intuitionistic sequent calculus with explicit weakening and contraction. We study a system derived from /\-Gtz of Espirito Santo by adding explicit operators for weakening and contraction, which we call l/\-Gtz. This system contains only linear terms. For the proposed calculus we introduce the type assignment system with simple types. The presented system has a natural diagrammatic representation, which is used for proving the subject reduction property. We prove the strong normalisation property by embedding l/\-Gtz into the simply typed /\lxr calculus of Kesner and Lengrand.

Document type :

Conference papers

Domain :

Computer Science [cs] / Mathematical Software [cs.MS]

Mathematics [math] / Logic [math.LO]

Complete list of metadatas

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00654762
Contributor : Pierre Lescanne <>
Submitted on : Thursday, December 22, 2011 - 8:52:28 PM
Last modification on : Tuesday, April 24, 2018 - 1:52:39 PM

Intuitionistic Sequent-Style Calculus with Explicit Structural Rules

Identifiers

Collections

Citation

Export

Metrics

138

Contact

Intuitionistic Sequent-Style Calculus with Explicit Structural Rules

Identifiers

Collections

Citation

Export

Share

Metrics

138

Contact