Abstract
We show how Modified Bar-Recursion, a variant of Spector's Bar-Recursion due to Berger and Oliva can be used to realize the Axiom of Countable Choice in Parigot's Lambda-Mu-calculus, a direct-style language for the representation and evaluation of classical proofs. We rely on Hyland-Ong innocent games. They provide a model for the instances of the axiom of choice usually used in the realization of classical choice with Bar-Recursion, and where, moreover, the standard datatype of natural numbers is in the image of a CPS-translation. © Springer International Publishing 2013.
Cite
CITATION STYLE
Blot, V., & Riba, C. (2013). On bar recursion and choice in a classical setting. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8301 LNCS, pp. 349–364). https://doi.org/10.1007/978-3-319-03542-0_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
