Computational interpretation of classical logic with explicit structural rules

Abstract : We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contraction. These structural rules introduce explicit erasure and duplication of terms, respectively. We present a type system for which we prove the type-preservation under reduction. A mutual relation with classical calculus featuring implicit structural rules has been studied in detail. From this analysis we derive strong normalisation property.
Liste complète des métadonnées

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00681296
Contributeur : Pierre Lescanne <>
Soumis le : mercredi 21 mars 2012 - 10:56:59
Dernière modification le : mardi 24 avril 2018 - 13:52:48
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 17:04:42

Fichiers

arxiv_classical.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : ensl-00681296, version 1
  • ARXIV : 1203.4754

Collections

Citation

Silvia Ghilezan, Pierre Lescanne, Dragisa Zunic. Computational interpretation of classical logic with explicit structural rules. 2012. 〈ensl-00681296〉

Partager

Métriques

Consultations de la notice

262

Téléchargements de fichiers

65