TITLE: Introduction to functional interpretations
QUESTION [3 upvotes]: Any good recomendations for an introduction to functional interpretations? I understand this is a little vague but i haven't had much contact with the area. I am particularly interested in the intuitionistic logic and wanted to get to know (possibly with some historical context also) some classical interpretations, namely: Modified Realizability, Gödel's functional interpretation and Diller-Nahm interpretation.

REPLY [5 votes]: You could try Ulrich Kohlenbach: "Applied Proof Theory: Proof Interpretations and their Use in Mathematics". Springer Monographs in Mathematics, 2008. Probably it is a big shot for your question, but it addresses

Systems of intuitionistic logic and arithmetic
No-Counterexample Interpretation (Kreisel)
Modified Realizability (Kreisel)
Functional (Dialectica) Interpretation (Gödel)
Applications of Functional Interpretation in mathematics

The historical context is usually outlined at the end of the respective chapters.
{"set_name": "stack_exchange", "score": 3, "question_id": 720130}