Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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.
Complete list of metadatas

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00681296
Contributor : Pierre Lescanne <>
Submitted on : Wednesday, March 21, 2012 - 10:56:59 AM
Last modification on : Wednesday, November 20, 2019 - 3:14:41 AM
Long-term archiving on: : Wednesday, December 14, 2016 - 5:04:42 PM

Files

arxiv_classical.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

503

Files downloads

90