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

`http://hdl.handle.net/1822/20889`

Title: | Monadic translation of classical sequent calculus |

Author(s): | Espírito Santo, José Matthes, Ralph Nakazawa, Koji Pinto, Luís F. |

Issue date: | 2013 |

Publisher: | Cambridge University Press |

Journal: | Mathematical 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. |

Type: | Article |

Description: | Em publicação |

URI: | http://hdl.handle.net/1822/20889 |

DOI: | 10.1017/s0960129512000436 |

ISSN: | 0960-1295 |

Peer-Reviewed: | yes |

Access: | Open access |

Appears in Collections: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals |