Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Constructive reverse mathematics is reverse mathematics carried out in Bishop-style constructive mathematics (BISH)---that is, using intuitionistic logic and, where necessary, constructive ZF set theory. There are two primary foci of constructive reverse mathematics:

first, investigating which constructive principles are necessary to prove a given constructive theorem;

secondly, investigating what non-constructive principles are necessary additions to BISH in order to prove a given non-constructive theorem.

I will present work on constructive reverse mathematics, carried out with Josef Berger and Hannes Diener. The main theme of the talk is the connection between the antithesis of Specker's theorem, various continuity properties, versions of the fan theorem, and Ishihara's principle.