some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

   Volume 11 (2015)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 12 (2016)

   Volume 13 (2017)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 11, ISSUE 4, PAPER 22


Typed realizability for first-order classical analysis

©Valentin Blot, University of Bath

Abstract
We describe a realizability framework for classical first-order 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 G"odel'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 Π02 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.

Publication date: December 31, 2015

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-11(4:22)2015

Hit Counts: 2223

Creative Commons