Polynomials and Dialectica categories

Martin Hyland, University of Cambridge. Part of the Logic Seminar Series.

This talk has two aims. First I shall give a simple concrete example of thinking in the style of Gödel’s functional interpretation. I hope that it will provide some modest motivation for the second part of the talk in which I shall give a survey of Gödel inspired interpretations of type theory.