\documentclass[a4paper]{article}
\usepackage{amssymb}
\pagestyle{empty}
\hoffset=-40pt
\voffset=-20pt
\textwidth 15.3cm
\textheight 22cm % to fit our printers

\begin{document}

\begin{center}{\huge Sequent Calculus and Computation}\end{center}
\begin{center}{\large Hugo Herbelin}\end{center}
\begin{center}{\large INRIA, France}\end{center}

\bigskip
\large

Gentzen's LJ and LK sequent calculi enjoy the subformula property.
For this reason, they are interesting both from a theoretical point of
view (consistency proofs, ...) and from a practical one (automated
deduction, ...). However, in contrast with intuitionistic natural
deduction (NJ) which is in correspondence with lambda-calculus, there
is no "clear" computational aspects for these calculi.

Of course, at least on the intuitionistic side, genuine Gentzen's
proof of cut elimination implicitly provides with a computational
contents of sequent calculi proofs. But how to justify it with respect
to other cut elimination proofs? There are also Tait's proof based
on an inversion lemma, Zucker's and Pottinger's cut-elimination
inherited from Prawitz's translation of LJ into NJ, ... and even other
variants of the Hauptsatz by Gentzen?

Moreover, Prawitz's translation maps different proofs of LJ to the same
NJ proof and then to the same lambda-term. How to understand it?

We show that, through Curry-Howard isomorphism, the cut rule can
be seen as an explicit operation of substitution. This leads to
a functional interpretation of LJ proofs based on a variant of
lambda-calculus temptatively called lambda-bar-calculus. Cut
elimination rules can then be understood as reduction rules for
the lambda-bar-calculus.

This functional notation suggests to put the emphasis not on LJ but
rather on a computationally better-behaved restriction of it call
LJT.

The mu construction of Parigot can be added to lambda-bar-calculus in
order to extend the functional interpretation to LK and LKT. A
connection can be seen between LJT and call-by-name evaluation and
between LJQ (a dual version of LJT) and call-by-value evaluation as
well. Strong normalisation results can be established.

Besides this functional interpretation of LJ and LK proofs, an
"interactive" interpretation of proofs of some various sequent calculi
as winning strategies in a two-players game (following Lorenzen and
Coquand) can be made.

The talk will cover (parts of) these computational interpretations.

\end{document}