Applications of inductive definitions and choice principles to program synthesis - Monika Seisenberger (Oxford Logic Guides, 2005)