Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
Stéphane Lengrand · Electronic Notes in Theoretical Computer Science · 2003
We present a typed calculus λξ isomorphic to the implicational fragment of the classical sequent calculus LK. Reductions in LK eliminate the cut-rule by local rewriting steps, which correspond to the evaluation of explicit substitutions in the calculus. This bridges the gap between Curien and Herbelinʼns λ μmu;-calculus and Urbanʼns rewriting system for proofs. Encodings of one into the other are defined, and from one of them we derive the strong normalization of λ μmu;. Identifying two reduction strategies CBV and CBN in Urban's rewriting system enables us to derive two corresponding semantics of continuations from those of λ μmu;, via the other encoding.