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

We present a version of Herbelin’s λ ¯ μ -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.