Computational interpretation of classical logic with explicit structural rules

TL;DR

This paper introduces a calculus linking classical logic and computation via explicit structural rules, proving type-preservation and strong normalization, thus clarifying the computational content of classical logic with explicit erasure and duplication.

Contribution

It provides a new calculus with explicit structural rules for classical logic, establishing type-preservation and strong normalization, and analyzing its relation to implicit structural rule calculus.

Findings

Type-preservation under reduction is proven.

Strong normalization property is derived.

Explicit structural rules correspond to erasure and duplication.

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.