Call-by-name reduction and cut-elimination in classical logic

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)

Abstract

We present a version of Herbelin's over(λ, -) μ-calculus in the call-by-name setting to study the precise correspondence between normalization and cut-elimination in classical logic. Our translation of λ μ-terms into a set of terms in the calculus does not involve any administrative redexes, in particular η-expansion on μ-abstraction. The isomorphism preserves β, μ-reduction, which is simulated by a local-step cut-elimination procedure in the typed case, where the reduction system strictly follows the " cut=redex" paradigm. We show that the underlying untyped calculus is confluent and enjoys the PSN (preservation of strong normalization) property for the isomorphic image of λ μ-calculus, which in turn yields a confluent and strongly normalizing local-step cut-elimination procedure for classical logic.

Original languageEnglish
Pages (from-to)38-65
Number of pages28
JournalAnnals of Pure and Applied Logic
Volume153
Issue number1-3
DOIs
Publication statusPublished - 2008 Apr

Keywords

  • Classical logic
  • Curry-Howard correspondence
  • Cut-elimination
  • Sequent calculus
  • Strong normalization

ASJC Scopus subject areas

  • Logic

Fingerprint Dive into the research topics of 'Call-by-name reduction and cut-elimination in classical logic'. Together they form a unique fingerprint.

Cite this