Espírito Santo, José and Matthes, Ralph and Nakazawa, Koji and Pinto, Luís Monadic translation of classical sequent calculus. (2013) Mathematical Structures in Computer Science, 23 (6). 11111162. ISSN 09601295

(Document in English)
PDF (Author's version)  Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 386kB 
Official URL: http://dx.doi.org/10.1017/S0960129512000436
Abstract
We study monadic translations of the callbyname (cbn) and callbyvalue (cbv) fragments of the classical sequent calculus ${\overline{\lambda}\mu\tilde{\mu}}$ due to Curien and Herbelin, and give modular and syntactic proofs of strong normalisation. The target of the translations is a new metalanguage for classical logic, named monadic λμ. This language 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 μreduction rule is replaced by a rule expressing the interaction between monadic binding and μabstraction. Our monadic translations produce very tight simulations of the respective fragments of ${\overline{\lambda}\mu\tilde{\mu}}$ within monadic λμ, with reduction steps of ${\overline{\lambda}\mu\tilde{\mu}}$ being translated in a 1–1 fashion, except for β steps, which require two steps. The monad of monadic λμ can be instantiated to the continuations monad so as to ensure strict simulation of monadic λμ within simply typed λcalculus with β and ηreduction. Through strict simulation, the strong normalisation of simply typed λcalculus is inherited by monadic λμ, and then by cbn and cbv ${\overline{\lambda}\mu\tilde{\mu}}$, thus reproving strong normalisation in an elementary syntactical way for these fragments of ${\overline{\lambda}\mu\tilde{\mu}}$, and establishing it for our new calculus. These results extend to secondorder logic, with polymorphic λcalculus as the target, giving new strong normalisation results for classical secondorder logic in sequent calculus style. CPS translations of cbn and cbv ${\overline{\lambda}\mu\tilde{\mu}}$ with the strict simulation property are obtained by composing our monadic translations with the continuationsmonad instantiation. In an appendix to the paper, we investigate several refinements of the continuationsmonad instantiation in order to obtain in a modular way improvements of the CPS translations enjoying extra properties like simulation by cbv βreduction or reduction of administrative redexes at compile time.
Item Type:  Article 

Additional Information:  Thanks to CUP editor. The definitive version is available at http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9053923&fileId=S0960129512000436 
HAL Id:  hal01138759 
Audience (journal):  International peerreviewed journal 
Uncontrolled Keywords:  
Institution:  French research institutions > Centre National de la Recherche Scientifique  CNRS (FRANCE) Université de Toulouse > Institut National Polytechnique de Toulouse  Toulouse INP (FRANCE) Université de Toulouse > Université Toulouse III  Paul Sabatier  UT3 (FRANCE) Université de Toulouse > Université Toulouse  Jean Jaurès  UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole  UT1 (FRANCE) Other partners > Kyoto University (JAPAN) Other partners > Universidade do Minho (PORTUGAL) 
Laboratory name:  
Statistics:  download 
Deposited On:  02 Apr 2015 14:16 
Repository Staff Only: item control page