License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.13
URN: urn:nbn:de:0030-drops-59913
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5991/
Go to the corresponding LIPIcs Volume Portal

Blot, Valentin

Classical Extraction in Continuation Models

pdf-format:
LIPIcs-FSCD-2016-13.pdf (0.5 MB)

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 Pi^0_2 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.

BibTeX - Entry

@InProceedings{blot:LIPIcs:2016:5991,
  author =	{Valentin Blot},
  title =	{{Classical Extraction in Continuation Models}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5991},
  URN =		{urn:nbn:de:0030-drops-59913},
  doi =		{10.4230/LIPIcs.FSCD.2016.13},
  annote =	{Keywords: Extraction, Classical Logic, Control Operators, Game Semantics}
}

Keywords: Extraction, Classical Logic, Control Operators, Game Semantics
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI