Departamento de Matemática
Universidade do Minho
Thursday, 2 December 2010, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: Classical logic gives a meaningful way to extend the basic setting of functional programming provided by lambda-calculus and intuitionistic logic, where control operators like call-cc acquire a logical foundation. In particular, its formulation in the sequent calculus format has been successfully used, for example, to account for dualities in computation.
It is known that monads are an useful concept to factor continuation-passing style (cps) translation of lambda-calculus. Specifically, Moggi's monadic meta-language can be used to factor traditional cps translations of call-by-name (cbn) and call-by-value (cbv) lambda-calculus.
In this seminar, I will present ongoing work on finding a similar decomposition for classical sequent calculus, but with an additional concern: the guarantee that our translations strictly simulate reduction (i.e. one step in the source calculus implies one or more steps in the target), so that strong normalisation of the target can be inherited by the source.
The ideas have been developed for the cbn and the cbv fragments of the classical sequent calculus lambda-bar-mu-mu-tilde by Curien and Herbelin. This, in particular, led us: (i) to the definition of a meta-language for classical logic, which is a monadic reworking of Parigot's lambda-mu-calculus, and whose intuitionistic restriction is a variant of Moggi's meta-language; (ii) to cps translations of cbn and cbv lambda-bar-mu-mu-tilde into simply-typed lambda-calculus that strictly simulate reductions, hence to a new elementary proof of strong normalisation for these fragments of lambda-bar-mu-mu-tilde. The results readily extend to second-order logic, with polymorphic lambda-calculus as target, giving new strong normalisation results.
(Joint work with José Espírito Santo, Ralph Matthes and Koji Nakazawa.)