Classical extraction in continuation models

Valentin Blot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We use the control features of continuation models to interpret proofs in first-order classical theories. This interpretation is suitable for extracting algorithms from proofs of Π02 formulas. It is fundamentally different from the usual direct interpretation, which is shown to be equivalent to Friedman's trick. The main difference is that atomic formulas and natural numbers are interpreted as distinct objects. Nevertheless, the control features inherent to the continuation models permit extraction using a special "channel" on which the extracted value is transmitted at toplevel without unfolding the recursive calls. We prove that the technique fails in Scott domains, but succeeds in the refined setting of Laird's bistable bicpos, as well as in game semantics.

Original languageEnglish
Title of host publicationLeibniz International Proceedings in Informatics, LIPIcs, 2016
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages13.1-13.17
Number of pages17
Volume52
ISBN (Print)9783959770101
DOIs
Publication statusPublished - 1 Jun 2016
Event1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal
Duration: 22 Jun 201626 Jun 2016

Conference

Conference1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
CountryPortugal
CityPorto
Period22/06/1626/06/16

Keywords

  • Classical logic
  • Control operators
  • Extraction
  • Game semantics

Fingerprint Dive into the research topics of 'Classical extraction in continuation models'. Together they form a unique fingerprint.

  • Projects

  • Cite this

    Blot, V. (2016). Classical extraction in continuation models. In Leibniz International Proceedings in Informatics, LIPIcs, 2016 (Vol. 52, pp. 13.1-13.17). [13] Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2016.13