War Time Proofs and Futuristic Programs

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 forties he came up with the ingenious idea of interpreting any formula of arithmetic as a formula of the shape ∃𝑢 : U∀𝑥 : X.A_𝐷(𝑢,𝑥) where A_𝐷 is quantifier-free. This was his famous Dialectica interpretation, published in 1958. Some 30 years after following Hyland's suggestion, I showed how that Gödel 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.

Valeria de Paiva is a mathematician and AI principal scientist at the Topos Institute, working on natural language processing, logical inference, and all kinds of semantics, especially Dialectica categories. Before Topos, Valeria worked at top industry NLP labs, including Samsung Research America, Nuance, Deem, Cuil, and for many years at Xerox PARC. Before that, she was a professor at the University of Birmingham, UK. She is very keen on making sure that women are not too short-changed in their professional lives. For that, she maintains the “Women in Logic” website, Facebook group, and blog, helps the ACM-W Scholarship program, and started the international workshop “Women in Logic”, now in its 7th year.

• Web Presence: https://vcvpaiva.github.io/
• Twitter: https://twitter.com/valeriadepaiva
• Github: https://github.com/vcvpaiva