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.

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

Submitted 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

38 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, Certified abstract machines for skeletal semantics, pp. 55-67, 2022, Philadelphia PA USA, 10.1145/3497775.3503676, https://hal.inria.fr/hal-03466807.

Maciej Buszka;Dariusz Biernacki, arXiv (Cornell University), Automating the Functional Correspondence Between Higher-Order Evaluators and Abstract Machines, pp. 38-59, 2022, 10.1007/978-3-030-98869-2_3, https://arxiv.org/abs/2108.07132.

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, Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Selective CPS transformation for shift and reset, pp. 40-52, 2017, Los Angeles CA USA, 10.1145/3162069.

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

Malgorzata Biernacka;Dariusz Biernacki;Serguei Lenglet;Piotr Polesiuk;Damien Pous;et al., Fully abstract encodings of λ-calculus in HOcore through abstract machines, pp. 1-12, 2017, Reykjavik, Iceland, 10.1109/lics.2017.8005118, https://hal.inria.fr/hal-01507625.

Neil Sculthorpe;Paolo Torrini;Peter D. Mosses, 2016, A Modular Structural Operational Semantics for Delimited Continuations, arXiv (Cornell University), 212, pp. 63-80, 10.4204/eptcs.212.5.

Dariusz Biernacki;Olivier Danvy;Kevin Millikin, 2015, A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations, Scopus (Elsevier), 38, 1, pp. 1-25, 10.1145/2794078, http://delivery.acm.org/10.1145/2800000/2794078/a2-biernacki.pdf?ip=192.38.33.14&id=2794078&acc=ACTIVE%20SERVICE&key=36332CD97FA87885%2E318148A04E30A4A4%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35&CFID=756601986&CFTOKEN=57655238&__acm__=1456493344_ea1db1105f3f8a1517d305024b667b39.

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, Environmental Bisimulations for Delimited-Control Operators, pp. 333-348, 2013, 10.1007/978-3-319-03542-0_24, https://hal.inria.fr/hal-00903839.

Małgorzata Biernacka;Dariusz Biernacki;Sergueï Lenglet;Marek Materzok, 2013, Proving termination of evaluation for System F with control operators, arXiv (Cornell University), 127, pp. 15-29, 10.4204/eptcs.127.2.

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

Álvaro García-Pérez;Pablo Nogueira;Juan José Moreno-Navarro, UPM Digital Archive (Technical University of Madrid), Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order, pp. 85-96, 2013, Madrid Spain, 10.1145/2505879.2505887, http://oa.upm.es/30153/.

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

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

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

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

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

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

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

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

Malgorzata Biernacka;Dariusz Biernacki, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, Context-based proofs of termination for typed delimited-control operators, pp. 289-300, 2009, Coimbra Portugal, 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, https://doi.org/10.1016/j.jcss.2009.10.004.

Olivier Danvy, 2008, Defunctionalized interpreters for programming languages, CiteSeer X (The Pennsylvania State University), 43, 9, pp. 131-142, 10.1145/1411203.1411206, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.685.1361.

Olivier Danvy;Jacob Johannsen, CiteSeer X (The Pennsylvania State University), Inter-deriving Semantic Artifacts for Object-Oriented Programming, pp. 1-16, 2008, 10.1007/978-3-540-69937-8_1, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.165.966.

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, Higher-Order 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, CiteSeer X (The Pennsylvania State University), 9, 1, pp. 6, 10.1145/1297658.1297664, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.164.9540.

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

Yukiyoshi Kameyama, 2007, Axioms for control operators in the CPS hierarchy, CiteSeer X (The Pennsylvania State University), 20, 4, pp. 339-369, 10.1007/s10990-007-9009-x, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.8825.

Oleg Kiselyov;Chung-chieh Shan;Amr Sabry, 2006, Delimited dynamic binding, CiteSeer X (The Pennsylvania State University), 41, 9, pp. 26-37, 10.1145/1160074.1159808, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8798.

Oleg Kiselyov;Chung-chieh Shan;Amr Sabry, CiteSeer X (The Pennsylvania State University), Delimited dynamic binding, 2006, Portland Oregon USA, 10.1145/1159803.1159808, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8798.

Dariusz Biernacki;Olivier Danvy;Chung-chieh Shan, 2005, On the dynamic extent of delimited continuations, CiteSeer X (The Pennsylvania State University), 96, 1, pp. 7-17, 10.1016/j.ipl.2005.04.003, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.824.2136.

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, CiteSeer X (The Pennsylvania State University), Axioms for Delimited Continuations in the CPS Hierarchy, pp. 442-457, 2004, 10.1007/978-3-540-30124-0_34, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.153.1414.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1878 times.

This article's PDF has been downloaded 645 times.

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

Classifications

Bibliographic References

38 Documents citing this article

Share and export

Consultation statistics