Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs

Abstract

The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem – the epsilon calculus, modified realizability and the Dialectica interpretation – and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming.