Bar recursion in classical realisability : dependent choice and continuum hypothesis

DOI10.4230/LIPIcs.CSL.2016.25zbMath1434.03055arXiv1502.00112MaRDI QIDQ5278411

Jean-Louis Krivine

Publication date: 19 July 2017

Full work available at URL: https://arxiv.org/abs/1502.00112

zbMATH Keywords

set theory\(\lambda\)-calculusCurry-Howard correspondence

Mathematics Subject Classification ID

Consistency and independence results (03E35) Continuum hypothesis and Martin's axiom (03E50) Axiom of choice and related propositions (03E25) Combinatory logic and lambda calculus (03B40)

Related Items (3)

Programming and Proving with Classical Types ⋮ Stateful Realizers for Nonstandard Analysis ⋮ Unnamed Item

This page was built for publication: Bar recursion in classical realisability : dependent choice and continuum hypothesis