Intuitionistic Sequent-Style Calculus with Explicit Structural Rules

Pierre Lescanne 1 Silvia Ghilezan 2 Jelena Ivetic 2 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.
Type de document :
Communication dans un congrès
Nick Bezhanishvili, Sebastian Löbner, Kerstin Schwabe, Luca Spada. Logic, Language, and Computation - 8th International Tbilisi Symposium on Logic, Language, and Computation, Sep 2009, Bakuriani, Georgia. Springer, 6618, pp.101-124, 2011, Lecture Notes in Computer Science
Liste complète des métadonnées
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00654762
Contributeur : Pierre Lescanne <>
Soumis le : jeudi 22 décembre 2011 - 20:52:28
Dernière modification le : mardi 24 avril 2018 - 13:52:39

Identifiants

  • HAL Id : ensl-00654762, version 1

Collections

ENS-LYON | INRIA | LIP | INSMI | UNIV-LYON1

Citation

Pierre Lescanne, Silvia Ghilezan, Jelena Ivetic, Dragisa Zunic. Intuitionistic Sequent-Style Calculus with Explicit Structural Rules. Nick Bezhanishvili, Sebastian Löbner, Kerstin Schwabe, Luca Spada. Logic, Language, and Computation - 8th International Tbilisi Symposium on Logic, Language, and Computation, Sep 2009, Bakuriani, Georgia. Springer, 6618, pp.101-124, 2011, Lecture Notes in Computer Science. 〈ensl-00654762〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

97

Contact

support.ccsd.cnrs.fr
hal.support@ccsd.cnrs.fr
Logo CCSD