Valentin Blot - Typed realizability for first-order classical analysis

lmcs:1623 - Logical Methods in Computer Science, December 31, 2015, Volume 11, Issue 4 - https://doi.org/10.2168/LMCS-11(4:22)2015
Typed realizability for first-order classical analysisArticle

Authors: Valentin Blot

    We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed {\lambda}{\mu}-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ödel'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 {\Pi}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.


    Volume: Volume 11, Issue 4
    Published on: December 31, 2015
    Submitted on: April 15, 2015
    Keywords: Computer Science - Logic in Computer Science

    1 Document citing this article

    Consultation statistics

    This page has been seen 1705 times.
    This article's PDF has been downloaded 442 times.