Event Detail

Historians remind us that we cannot predict the future if we don’t understand the past. And the past sometimes has new explanations, if we look for them. I want to show you a particular instance of the Curry-Howard correspondence, based on the work of Kurt Gödel in the 40s that I claim is an example of this phenomenon of new explanations from the past. Gödel wanted to prove the consistency of arithmetic by restricted means. In the 40s he came up with the ingenious idea of interpreting any formula of arithmetic as a formula of the shape \exists u:U\forall x:X. A_D(u,x) where A_D is quantifier-free. This was his famous Dialectica interpretation, published in 1958. Some 30 years after that, following Hyland’s suggestion, I showed how Gödel’s idea corresponds to a kind of linear logic type theory. This was interesting then because Linear Logic was just beginning and people didn’t know how good for Computer Science it was going to be. Now, 35 years later, Linear Logic is used in many advanced programming languages and type systems, and more applications are expected. But we’re still explaining and extending the tricks of the old master, as I hope to show you.