Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Blot, Valentin http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-59913
URL:

Classical Extraction in Continuation Models

pdf-format:


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
Seminar: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue date: 2016
Date of publication: 2016


DROPS-Home | Fulltext Search | Imprint Published by LZI