Classical realizability is a technique for extracting computational content from classical proofs. It was introduced by Krivine in the middle of the 1990's combining ideas from traditional Kleene realizability and from logical translations from classical to intuitionistic logics. Its fundamental contribution is to put the notion of interaction (between a proof and a counter-proof, or between a program and its environment) in a central position explicitly. Subsequently, it provides enlightening descriptions of the computational behaviour of classical tautologies as synchronization mechanisms between threads of a program.

In this talk, I will survey the fundamental ideas that lead to the interactive study of proofs with the tools of classical realizability, in the original framework of the ?-calculus with control operators. I will show how these ideas relate to other models for proof systems (games, ludics…), how it can be extended to other models of computation and what it can teach us about the ongoing question of the proof-program correspondence for concurrent computation.