Skip to main content
SpringerLink
Log in

On Bar Recursion and Choice in a Classical Setting

  • Conference paper
Book cover Programming Languages and Systems (APLAS 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8301))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky, S., McCusker, G.: Call-by-Value Games. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 1–17. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  2. Amadio, R.M., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1998)

    Google Scholar 

  3. Berardi, S., Bezem, M., Coquand, T.: On the Computational Content of the Axiom of Choice. Journal of Symbolic Logic 63(2), 600–622 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  4. Berger, U., Oliva, P.: Modified bar recursion and classical dependent choice. Lecture Notes in Logic 20, 89–107 (2005)

    MathSciNet  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. Griffin, T.: A Formulae-as-Types Notion of Control. In: POPL 1990, pp. 47–58. ACM Press (1990)

    Google Scholar 

  7. Harmer, R.: Games and Full Abstraction for Nondeterministic Languages. PhD thesis, Imperial College, London (1999)

    Google Scholar 

  8. Hyland, J.M.E., Ong, C.-H.: On Full Abstraction for PCF: I, II, and III. Information and Computation 163(2), 285–408 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  9. Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer (2008)

    Google Scholar 

  10. 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)

    Google Scholar 

  11. Laird, J.: A Semantic analysis of control. PhD thesis, University of Edimbourgh (1998)

    Google Scholar 

  12. Miquel, A.: Existential witness extraction in classical realizability and via a negative translation. Logical Methods in Computer Science 7(2) (2011)

    Google Scholar 

  13. Oliva, P., Streicher, T.: On Krivine’s Realizability Interpretation of Classical Second-Order Arithmetic. Fundam. Inform. 84(2), 207–220 (2008)

    MathSciNet  MATH  Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. Selinger, P.: Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus. Mathematical Structures in Computer Science 11, 207–260 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  16. Simpson, S.G.: Subsystems of Second Order Arithmetic, 2nd edn. Perspectives in Logic. Cambridge University Press (2010)

    Google Scholar 

  17. Streicher, T.: A Classical Realizability Model araising from a Stable Model of Untyped Lambda-Calculus (unpublished Notes, 2013)

    Google Scholar 

  18. Streicher, T., Reus, B.: Classical Logic, Continuation Semantics and Abstract Machines. J. Funct. Program. 8(6), 543–572 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  19. Troelstra, A.S.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. LNM, vol. 344. Springer, Heidelberg (1973)

    Book  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ENS de Lyon, Université de Lyon, LIP, France

    Valentin Blot & Colin Riba

Authors
  1. Valentin Blot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Colin Riba
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Indiana University, 150 S. Woodlawn Avenue, 47405-7104, Bloomington, IN, USA

    Chung-chieh Shan

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation