An Operational Foundation for Delimited Continuations in the CPS Hierarchy

Malgorzata Biernacka; Dariusz Biernacki; Olivier Danvy

doi:10.2168/LMCS-1(2:5)2005

Malgorzata Biernacka ; Dariusz Biernacki ; Olivier Danvy - An Operational Foundation for Delimited Continuations in the CPS Hierarchy

lmcs:2269 - Logical Methods in Computer Science, November 8, 2005, Volume 1, Issue 2 - https://doi.org/10.2168/LMCS-1(2:5)2005

An Operational Foundation for Delimited Continuations in the CPS HierarchyArticle

Authors: Malgorzata Biernacka ; Dariusz Biernacki ; Olivier Danvy

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

Comment: 39 pages

https://doi.org/10.2168/LMCS-1(2:5)2005

Source: arXiv.org:cs/0508048

Volume: Volume 1, Issue 2

Published on: November 8, 2005

Imported on: April 1, 2005

Keywords: Computer Science - Logic in Computer Science, Computer Science - Programming Languages, D.1.1, F.3.2

Licence: arXiv.org - Assumed non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

37 Documents citing this article

Filip Sieczkowski;Mateusz Pyzik;Dariusz Biernacki, 2023, A General Fine-Grained Reduction Theory for Effect Handlers, Proceedings of the ACM on Programming Languages, 7, ICFP, pp. 511-540, 10.1145/3607848, https://doi.org/10.1145/3607848.

Guillaume Ambal;Sergueï Lenglet;Alan Schmitt, 2022, Certified abstract machines for skeletal semantics, pp. 55-67, 10.1145/3497775.3503676, https://inria.hal.science/hal-03466807.

Maciej Buszka;Dariusz Biernacki, 2022, Automating the Functional Correspondence Between Higher-Order Evaluators and Abstract Machines, Lecture notes in computer science, pp. 38-59, 10.1007/978-3-030-98869-2_3.

Dariusz Biernacki;Maciej Piróg;Piotr Polesiuk;Filip Sieczkowski, 2019, Abstracting algebraic effects, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-28, 10.1145/3290319, https://doi.org/10.1145/3290319.

Guannan Wei;James Decker;Tiark Rompf, 2018, Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl), Proceedings of the ACM on Programming Languages, 2, ICFP, pp. 1-28, 10.1145/3236800, https://doi.org/10.1145/3236800.

Dariusz Biernacki;Maciej Piróg;Piotr Polesiuk;Filip Sieczkowski, 2017, Handle with care: relational interpretation of algebraic effects and handlers, Proceedings of the ACM on Programming Languages, 2, POPL, pp. 1-30, 10.1145/3158096, https://doi.org/10.1145/3158096.

Kenichi Asai;Chihiro Uehara, 2017, Selective CPS transformation for shift and reset, Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 40-52, 10.1145/3162069.

Kenichi Asai;Chihiro Uehara, 2017, Selective CPS transformation for shift and reset, Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation - PEPM '18, pp. 40-52, 10.1145/3175493.3162069.

Neil Sculthorpe;Paolo Torrini;Peter D. Mosses, 2016, A Modular Structural Operational Semantics for Delimited Continuations, Electronic Proceedings in Theoretical Computer Science, 212, pp. 63-80, 10.4204/eptcs.212.5, https://doi.org/10.4204/eptcs.212.5.

Dariusz Biernacki;Olivier Danvy;Kevin Millikin, 2015, A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations, ACM Transactions on Programming Languages and Systems, 38, 1, pp. 1-25, 10.1145/2794078.

PAUL DOWNEN;ZENA M. ARIOLA, 2014, Delimited control and computational effects, Journal of Functional Programming, 24, 1, pp. 1-55, 10.1017/s0956796813000312, https://doi.org/10.1017/s0956796813000312.

Dariusz Biernacki;Sergueï Lenglet, 2013, Environmental Bisimulations for Delimited-Control Operators, arXiv (Cornell University), pp. 333-348, 10.1007/978-3-319-03542-0_24, http://arxiv.org/abs/1309.3919.

Małgorzata Biernacka;Dariusz Biernacki;Sergueï Lenglet;Marek Materzok, 2013, Proving termination of evaluation for System F with control operators, Electronic Proceedings in Theoretical Computer Science, 127, pp. 15-29, 10.4204/eptcs.127.2, https://doi.org/10.4204/eptcs.127.2.

Wojciech Jedynak;Małgorzata Biernacka;Dariusz Biernacki, 2013, An operational foundation for the tactic language of Coq, Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, pp. 25-36, 10.1145/2505879.2505890.

Álvaro García-Pérez;Pablo Nogueira;Juan José Moreno-Navarro, 2013, Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order, Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, pp. 85-96, 10.1145/2505879.2505887.

Asami Tanaka;Yukiyoshi Kameyama, 2012, A Call-by-Name CPS Hierarchy, Lecture notes in computer science, pp. 260-274, 10.1007/978-3-642-29822-6_21.

Dariusz Biernacki;Sergueï Lenglet, 2012, Normal Form Bisimulations for Delimited-Control Operators, pp. 47-61, 10.1007/978-3-642-29822-6_7, https://inria.hal.science/hal-01399951.

Malgorzata Biernacka;Dariusz Biernacki;Sergueï Lenglet, 2011, Typing control operators in the CPS hierarchy, pp. 149-160, 10.1145/2003476.2003498, https://hal.inria.fr/hal-00903834.

Marek Materzok;Dariusz Biernacki, 2011, Subtyping delimited continuations, Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, pp. 81-93, 10.1145/2034773.2034786.

Marek Materzok;Dariusz Biernacki, 2011, Subtyping delimited continuations, ACM SIGPLAN Notices, 46, 9, pp. 81-93, 10.1145/2034574.2034786.

Alexis Saurin, 2010, A Hierarchy for Delimited Continuations in Call-by-Name, Lecture notes in computer science, pp. 374-388, 10.1007/978-3-642-12032-9_26, https://doi.org/10.1007/978-3-642-12032-9_26.

Kenichi Asai;Arisa Kitani, 2010, Functional derivation of a virtual machine for delimited continuations, Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, pp. 87-98, 10.1145/1836089.1836101.

Noam Zeilberger, 2010, Polarity and the Logic of Delimited Continuations, 161, pp. 219-227, 10.1109/lics.2010.23.

Malgorzata Biernacka;Dariusz Biernacki, 2009, Context-based proofs of termination for typed delimited-control operators, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, pp. 289-300, 10.1145/1599410.1599446.

Olivier Danvy;Jacob Johannsen, 2009, Inter-deriving semantic artifacts for object-oriented programming, Journal of Computer and System Sciences, 76, 5, pp. 302-323, 10.1016/j.jcss.2009.10.004.

Olivier Danvy, 2008, Defunctionalized interpreters for programming languages, ACM SIGPLAN Notices, 43, 9, pp. 131-142, 10.1145/1411203.1411206.

Olivier Danvy;Jacob Johannsen, 2008, Inter-deriving Semantic Artifacts for Object-Oriented Programming, Lecture notes in computer science, pp. 1-16, 10.1007/978-3-540-69937-8_1.

Olivier Danvy;Kevin Millikin, 2008, A Rational Deconstruction of Landin's SECD Machine with the J Operator, Logical Methods in Computer Science, Volume 4, Issue 4, 10.2168/lmcs-4(4:12)2008, https://doi.org/10.2168/lmcs-4(4:12)2008.

Chung-chieh Shan, 2007, A static simulation of dynamic delimited control, LISP and Symbolic Computation, 20, 4, pp. 371-401, 10.1007/s10990-007-9010-4.

Małgorzata Biernacka;Olivier Danvy, 2007, A concrete framework for environment machines, ACM Transactions on Computational Logic, 9, 1, pp. 6, 10.1145/1297658.1297664.

Oleg Kiselyov;Chung-chieh Shan, 2007, A Substructural Type System for Delimited Continuations, Lecture notes in computer science, pp. 223-239, 10.1007/978-3-540-73228-0_17.

Yukiyoshi Kameyama, 2007, Axioms for control operators in the CPS hierarchy, LISP and Symbolic Computation, 20, 4, pp. 339-369, 10.1007/s10990-007-9009-x.

Oleg Kiselyov;Chung-chieh Shan;Amr Sabry, 2006, Delimited dynamic binding, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, pp. 26-37, 10.1145/1159803.1159808.

Oleg Kiselyov;Chung-chieh Shan;Amr Sabry, 2006, Delimited dynamic binding, ACM SIGPLAN Notices, 41, 9, pp. 26-37, 10.1145/1160074.1159808.

Dariusz Biernacki;Olivier Danvy;Chung-chieh Shan, 2005, On the dynamic extent of delimited continuations, Information Processing Letters, 96, 1, pp. 7-17, 10.1016/j.ipl.2005.04.003.

Olivier Danvy, 2005, From Reduction-based to Reduction-free Normalization, Electronic Notes in Theoretical Computer Science, 124, 2, pp. 79-100, 10.1016/j.entcs.2005.01.007, https://doi.org/10.1016/j.entcs.2005.01.007.

Yukiyoshi Kameyama, 2004, Axioms for Delimited Continuations in the CPS Hierarchy, Lecture notes in computer science, pp. 442-457, 10.1007/978-3-540-30124-0_34.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3274 times.

This article's PDF has been downloaded 803 times.