Paulo Oliva

School of Electronic Engineering and Computer Science
Queen Mary, University of London (QMUL)

Abstract. Functional interpretations provide us with a systematic way of translating logical dependencies into functional dependencies. The most well-known such interpretations include Kleene’s realizability, Kreisel’s modified realizability and Gödel’s Dialectica interpretation. In this series of lectures we will cover the basic concepts behind such functional interpretations, looking at each interpretation individually and then identifying the common features between them. We will also discuss the foundational motivations for the development of such interpretation as well as its more recent applications to program extraction from proofs and proof mining.