LIPIcs.CSL.2013.521.pdf
- Filesize: 0.53 MB
- 19 pages
Document
Axiomatizing Subtyped Delimited Continuations
Author
-
Part of:
Volume:
Computer Science Logic 2013 (CSL 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2013-09-02
Cite AsGet BibTex
Marek Materzok. Axiomatizing Subtyped Delimited Continuations. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 521-539, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.CSL.2013.521
https://doi.org/10.4230/LIPIcs.CSL.2013.521
Abstract
We present direct equational axiomatizations of the call-by-value lambda calculus with the control operators shift_0 and reset_0 that generalize Danvy and Filinski's shift and reset in that they allow for abstracting control beyond the top-most delimited continuation. We address an untyped version of the calculus as well as a typed version with effect subtyping. For each of the calculi we present a set of axioms that we prove sound and complete with respect to the corresponding CPS translation.
Keywords
- Delimited Continuations
- Continuation Passing Style
- Axiomatization
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads