On bar recursive interpretations of analysis
On bar recursive interpretations of analysis
Thomas Powell
2013 · DBLP: phd/ethos/Powell13
13 Citations
TLDR
It is proved that modified bar recursion (in the form of the implicitly controlled product of selection functions), open recursion, update recursion and the Berardi-BezemCoquand realizer for countable choice are all primitive recursively equivalent in the model of continuous functionals.
