Monadic translation of classical sequent calculus

Abstract

We study monadic translations of the call-by-name (cbn) and the call-by-value (cbv) fragments of the classical sequent calculus lambda-mu-mu~ by Curien and Herbelin and give modular and syntactic proofs of strong normalization. The target of the translations is a new meta-language for classical logic, named monadic lambda-mu . It is a monadic reworking of Parigot’s -calculus, where the monadic binding is confined to commands, thus integrating the monad with the classical features. Also its mu -reduction rule is replaced by one expressing the interaction between monadic binding and mu -abstraction. Our monadic translations produce very tight simulations of the respective fragments of lambda-mu-mu~ inside monadic lambda-mu , with reduction steps of lambda-mu-mu~ being translated in 1-1 fashion, except for beta-steps which require two steps. The monad of monadic lambda-mu can be instantiated to the continuations monad so as to ensure strict simulation of monadic lambda-mu inside simply-typed -calculus with beta- and eta -reduction. Through strict simulation, strong normalization of simply-typed -calculus is inherited to monadic lambda-mu and then to cbn and cbv lambda-mu-mu~, thus reproving in an elementary syntactical way strong normalization for these fragments of lambda-mu-mu~ and establishing it for our new calculus. These results extend to second-order logic, with polymorphic -calculus as target, giving new strong normalization results for classical second-order logic in sequent calculus style. CPS translations of cbn and cbv lambda-mu-mu~ with the strict simulation property are obtained by composing our monadic translations with the continuations-monad instantiation. In an appendix to the article we investigate several refinements of the continuations-monad instantiation in order to obtain in a modular way improvements of the CPS translations enjoying extra properties like simulation by cbv beta -reduction or reduction of administrative redexes at compile time.