Classical extraction in continuation models

Valentin Blot

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding


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
Number of pages17
ISBN (Print)9783959770101
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


Conference1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016


  • Classical logic
  • Control operators
  • Extraction
  • Game semantics


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

Cite this