Modified Bar Recursion
Ulrich Berger
April 2002 |
Abstract:
We introduce a variant of Spector's bar recursion (called
``modified bar recursion'') in finite types to give a realizability
interpretation of the classical axiom of countable choice allowing for the
extraction of witnesses from proofs of
![]() ![]() ![]() Available as PostScript, PDF, DVI. |