## Monadic translation of sequent calculus for classical logic

### Luís Pinto

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.)

Tarmo Uustalu

Last update 9.12.2010