Realizability as the Connection between Computable and Constructive Mathematics
Abstract:
These are lecture notes for a tutorial seminar which I gave at a satellite seminar of Computability and Complexity in Analysis 2005 in Kyoto. The main message of the notes is that computable mathematics is the realizability interpretation of constructive mathematics. The presentation is targeted at an audience which is familiar with computable mathematics but less so with constructive mathematics, category theory or realizability theory.
Note: I have revised the original version from August 23, 2005 and corrected the horrible error at the beginning of Section 2. I would appreciate reports on other mistakes that you find in these notes.