Computational interpretation of classical logic with explicit structural rules
Logic in Computer Science
2012-03-23 v1 Distributed, Parallel, and Cluster Computing
Logic
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.
Cite
@article{arxiv.1203.4754,
title = {Computational interpretation of classical logic with explicit structural rules},
author = {Silvia Ghilezan and Pierre Lescanne and Dragisa Zunic},
journal= {arXiv preprint arXiv:1203.4754},
year = {2012}
}