Projects per year
Abstract
In intuitionistic realizability like Kleene's or Kreisel's, the axiom of choice is trivially realized. It is even provable in MartinLöf's intuitionistic type theory. In classical logic, however, even the weaker axiom of countable choice proves the existence of noncomputable functions. This logical strength comes at the price of a complicated computational interpretation which involves strong recursion schemes like bar recursion. We take the best from both worlds and define a realizability model for arithmetic and the axiom of choice which encompasses both intuitionistic and classical reasoning. In this model two versions of the axiom of choice can coexist in a single proof: intuitionistic choice and classical countable choice. We interpret intuitionistic choice efficiently, however its premise cannot come from classical reasoning. Conversely, our version of classical choice is valid in full classical logic, but it is restricted to the countable case and its realizer involves bar recursion. Having both versions allows us to obtain efficient extracted programs while keeping the provability strength of classical logic.
Original language  English 

Title of host publication  LICS '16, Proceedings of the 31st Annual ACMIEEE Symposium on Logic in Computer Science 
Place of Publication  New York, U. S. A. 
Publisher  IEEE 
Pages  575584 
Number of pages  10 
ISBN (Print)  9781450343916 
DOIs  
Publication status  Published  5 Jul 2016 
Event  31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016  New York, USA United States Duration: 5 Jul 2016 → 8 Jul 2016 
Conference
Conference  31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 

Country  USA United States 
City  New York 
Period  5/07/16 → 8/07/16 
Fingerprint Dive into the research topics of 'Hybrid realizability for intuitionistic and classical choice'. Together they form a unique fingerprint.
Projects
 1 Finished

Semantic Types for Verified Program Behaviour
Engineering and Physical Sciences Research Council
28/02/14 → 31/07/17
Project: Research council