Departamento de Matemática
Universidade do Minho
Thursday, 2 August 2007, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: The Curry-Howard correspondence establishes connections between the simply typed lambda-calculus and the intuitionistic implicational fragment of natural deduction.
In this talk we present some experiments on analogous connections when natural deduction is replaced by sequent calculus and when new term-calculi, extending the simply typed lambda-calculus, are considered.
We will present some of the new features and issues related to these extended systems (e.g., the presence of generalised and multiary function application, the co-existence of reduction and permutative conversions and the existence of various classes of normal forms) and pay special attention to recent developments in these studies, which achieve continuation passing-style translations of intuitionistic sequent calculi into the lambda-calculus, with preservation of reduction.
Joint work with José Espírito Santo (Universidade do Minho) and partly with Maria João Frade (Universidade do Minho) and Ralph Matthes (CNRS and Université Toulouse III).