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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S., McCusker, G.: Call-by-Value Games. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 1–17. Springer, Heidelberg (1998)
Amadio, R.M., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1998)
Berardi, S., Bezem, M., Coquand, T.: On the Computational Content of the Axiom of Choice. Journal of Symbolic Logic 63(2), 600–622 (1998)
Berger, U., Oliva, P.: Modified bar recursion and classical dependent choice. Lecture Notes in Logic 20, 89–107 (2005)
Blot, V.: Realizability for peano arithmetic with winning conditions in HON games. In: Hasegawa, M. (ed.) TLCA 2013. LNCS, vol. 7941, pp. 77–92. Springer, Heidelberg (2013)
Griffin, T.: A Formulae-as-Types Notion of Control. In: POPL 1990, pp. 47–58. ACM Press (1990)
Harmer, R.: Games and Full Abstraction for Nondeterministic Languages. PhD thesis, Imperial College, London (1999)
Hyland, J.M.E., Ong, C.-H.: On Full Abstraction for PCF: I, II, and III. Information and Computation 163(2), 285–408 (2000)
Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer (2008)
Krivine, J.-L.: Realizability in classical logic. In: Interactive Models of Computation and Program Behaviour. Panoramas et synthèses, vol. 27, pp. 197–229. Société Mathématique de France (2009)
Laird, J.: A Semantic analysis of control. PhD thesis, University of Edimbourgh (1998)
Miquel, A.: Existential witness extraction in classical realizability and via a negative translation. Logical Methods in Computer Science 7(2) (2011)
Oliva, P., Streicher, T.: On Krivine’s Realizability Interpretation of Classical Second-Order Arithmetic. Fundam. Inform. 84(2), 207–220 (2008)
Parigot, M.: Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Selinger, P.: Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus. Mathematical Structures in Computer Science 11, 207–260 (2001)
Simpson, S.G.: Subsystems of Second Order Arithmetic, 2nd edn. Perspectives in Logic. Cambridge University Press (2010)
Streicher, T.: A Classical Realizability Model araising from a Stable Model of Untyped Lambda-Calculus (unpublished Notes, 2013)
Streicher, T., Reus, B.: Classical Logic, Continuation Semantics and Abstract Machines. J. Funct. Program. 8(6), 543–572 (1998)
Troelstra, A.S.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. LNM, vol. 344. Springer, Heidelberg (1973)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Blot, V., Riba, C. (2013). On Bar Recursion and Choice in a Classical Setting. In: Shan, Cc. (eds) Programming Languages and Systems. APLAS 2013. Lecture Notes in Computer Science, vol 8301. Springer, Cham. https://doi.org/10.1007/978-3-319-03542-0_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-03542-0_25
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03541-3
Online ISBN: 978-3-319-03542-0
eBook Packages: Computer ScienceComputer Science (R0)