23/04/2016, 12:15 — 13:15 — Abreu Faro Amphitheatre
José Espírito Santo, Centro de Matemática, Universidade do Minho

Curry-Howard for sequent calculus at last

What do variables in sequent calculus proof terms stand for? What is co-control and what is a co-continuation?  Answering these questions is required, if a full understanding of the Curry-Howard isomorphism for sequent calculus is to be achieved. This talk is about a recent answer to these questions, which led to the interpretation that sequent calculus is a formal vector notation (for lambda-terms) with first-class co-control.