Computational interpretation of classical logic with explicit structural rules
From MaRDI portal
Publication:6231774
arXiv1203.4754MaRDI QIDQ6231774FDOQ6231774
Authors: Silvia Ghilezan, Pierre Lescanne, Dragiša Žunić 
Publication date: 21 March 2012
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.
This page was built for publication: Computational interpretation of classical logic with explicit structural rules
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6231774)
