Please use this identifier to cite or link to this item:

TitleMonadic translation of classical sequent calculus
Author(s)Espírito Santo, José
Matthes, Ralph
Nakazawa, Koji
Pinto, Luís F.
Issue date2013
PublisherCambridge University Press
JournalMathematical Structures in Computer Science
Abstract(s)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.
DescriptionEm publicação
AccessOpen access
Appears in Collections:CMAT - Artigos em revistas com arbitragem / Papers in peer review journals

Files in This Item:
File Description SizeFormat 
main.pdf480,45 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID