Realizability: a machine for Analysis and Set Theory
Jean-Louis Krivine · 2006
In this tutorial, we introduce the Curry-Howard (proof-program) correspondence which is usually restricted to intuitionistic logic. We explain how to extend this correspondence to the whole of mathematics and we build a simple suitable machine for this.