Projects per year
Abstract
We describe a realizability framework for classical firstorder logic in which realizers live in (a model of) typed λμcalculus. This allows a direct interpretation of classical proofs, avoiding the usual negative translation to intuitionistic logic. We prove that the usual terms of Godel’s system T realize the axioms of Peano arithmetic, and that under some assumptions on the computational model, the bar recursion operator realizes the axiom of dependent choice. We also perform a proper analysis of relativization, which allows for less technical proofs of adequacy. Extraction of algorithms from proofs of (formula presented) formulas relies on a novel implementation of Friedman’s trick exploiting the control possibilities of the language. This allows to have extracted programs with simpler types than in the case of negative translation followed by intuitionistic realizability.
Original language  English 

Journal  Logical Methods in Computer Science 
Volume  11 
Issue number  4 
DOIs  
Publication status  Published  31 Dec 2015 
Keywords
 Axiom of choice
 Barrecursion
 Classical realizability
 Lambdamu calculus
Fingerprint Dive into the research topics of 'Typed realizability for firstorder classical analysis'. 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