Document Open Access Logo

Classical Extraction in Continuation Models

Author Valentin Blot

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.13.pdf
  • Filesize: 465 kB
  • 17 pages

Document Identifiers

Author Details

Valentin Blot

Cite AsGet BibTex

Valentin Blot. Classical Extraction in Continuation Models. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.13

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.
Keywords
  • Extraction
  • Classical Logic
  • Control Operators
  • Game Semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Samson Abramsky, Kohei Honda, and Guy McCusker. A Fully Abstract Game Semantics for General References. In 13th Annual IEEE Symposium on Logic in Computer Science, pages 334-344. IEEE Computer Society, 1998. Google Scholar
  2. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full Abstraction for PCF. Information and Computation, 163(2):409-470, 2000. Google Scholar
  3. Roberto Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. Google Scholar
  4. Stefano Berardi, Marc Bezem, and Thierry Coquand. On the Computational Content of the Axiom of Choice. Journal of Symbolic Logic, 63(2):600-622, 1998. Google Scholar
  5. Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg. Refined program extraction from classical proofs. Annals of Pure and Applied Logic, 114(1-3):3-25, 2002. Google Scholar
  6. Ulrich Berger and Paulo Oliva. Modified bar recursion and classical dependent choice. In Logic Colloquium 2001, Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, volume 20 of Lecture Notes in Logic, pages 89-107. A K Peters, Ltd., 2005. Google Scholar
  7. Valentin Blot and Colin Riba. On Bar Recursion and Choice in a Classical Setting. In 11th Asian Symposium on Programming Languages and Systems, volume 8301 of Lecture Notes in Computer Science, pages 349-364. Springer, 2013. Google Scholar
  8. Harvey Friedman. Classically and intuitionistically provably recursive functions. In Gert Müller and Dana Scott, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21-27. Springer, 1978. Google Scholar
  9. Timothy Griffin. A Formulae-as-Types Notion of Control. In 17th Symposium on Principles of Programming Languages, pages 47-58. ACM Press, 1990. Google Scholar
  10. Russ Harmer. Games and full abstraction for non-deterministic languages. PhD thesis, Imperial College London (University of London), 1999. Google Scholar
  11. Hugo Herbelin. On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. In 7th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Mathematics, pages 209-220. Springer, 2005. Google Scholar
  12. Martin Hofmann and Thomas Streicher. Completeness of Continuation Models for λμ-Calculus. Information and Computation, 179(2):332-355, 2002. Google Scholar
  13. Martin Hyland and Luke Ong. On Full Abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000. Google Scholar
  14. Stephen Cole Kleene. On the Interpretation of Intuitionistic Number Theory. Journal of Symbolic Logic, 10(4):109-124, 1945. Google Scholar
  15. Jean-Louis Krivine. Dependent choice, `quote' and the clock. Theoretical Computer Science, 308(1-3):259-276, 2003. Google Scholar
  16. Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthèses, 27:197-229, 2009. Google Scholar
  17. Yves Lafont, Bernhard Reus, and Thomas Streicher. Continuations Semantics or Expressing Implication by Negation. Technical Report 93-21, Ludwig-Maximilians-Universität, München, 1993. Google Scholar
  18. James Laird. Full Abstraction for Functional Languages with Control. In 12th Annual IEEE Symposium on Logic in Computer Science, pages 58-67. IEEE Computer Society, 1997. Google Scholar
  19. James Laird. Bistable Biorders: A Sequential Domain Theory. Logical Methods in Computer Science, 3(2), 2007. Google Scholar
  20. Alexandre Miquel. Existential witness extraction in classical realizability and via a negative translation. Logical Methods in Computer Science, 7(2), 2011. Google Scholar
  21. Hanno Nickau. Hereditarily Sequential Functionals. In Third International Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science, pages 253-264. Springer, 1994. Google Scholar
  22. Paulo Oliva and Thomas Streicher. On Krivine’s Realizability Interpretation of Classical Second-Order Arithmetic. Fundamenta Informaticae, 84(2):207-220, 2008. Google Scholar
  23. Michel Parigot. λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In 3rd International Conference on Logic Programming and Automated Reasoning, volume 624 of Lecture Notes in Computer Science, pages 190-201. Springer, 1992. Google Scholar
  24. Christophe Raffalli. Getting results from programs extracted from classical proofs. Theoretical Computer Science, 323(1-3):49-70, 2004. Google Scholar
  25. Peter Selinger. Control categories and duality: on the categorical semantics of the λμ calculus. Mathematical Structures in Computer Science, 11(2):207-260, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact