research-article

An approach to call-by-name delimited continuations

Authors:

Silvia GhilezanAuthors Info & Claims

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 383 - 394

https://doi.org/10.1145/1328438.1328484

Published: 07 January 2008 Publication History

Abstract

We show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al's call-by-value calculus of delimited control, an extension of λμ-calculus with delimited control known to be equationally equivalent to Danvy and Filinski's calculus with shift and reset. Our main result then is that de Groote and Saurin's variant of λμ-calculus is equivalent to a canonical call-by-name variant of Ariola et al's calculus. The rest of the paper is devoted to a comparative study of the call-by-name and call-by-value variants of Ariola et al's calculus, covering in particular the questions of simple typing, operational semantics, and continuation-passing-style semantics. Finally, we discuss the relevance of Ariola et al's calculus as a uniform framework for representing different calculi of delimited continuations, including "lazy" variants such as Sabry's shift and lazy reset calculus.

References

[1]

Zena M. Ariola and Hugo Herbelin. Control reduction theories: the benefit of structural substitution. J. Funct. Program., 2007. Includes a Historical Note by Matthias Felleisen. To appear.

Digital Library

[2]

Zena M. Ariola, Hugo Herbelin, and Amr Sabry. A type-theoretic foundation of delimited continuations. Higher Order and Symbolic Computation, 2007. To appear.

Digital Library

[3]

Kensuke Baba, Sachio Hirokawa, and Ken-etsu Fujita. Parallel reduction in type free λμ-calculus. Electronic Notes in Theoretical Computer Science, 42: 52--66, 2001.

[4]

Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations. Technical Report 03-41, BRICS, University of Aarhus, Denmark, 2003.

[5]

Dariusz Biernacki and Olivier Danvy. On the dynamic extent of delimited continuations. Technical Report 05-2, BRICS, University of Aarhus, Denmark, 2005.

[6]

Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP 2000, Montreal, Canada, September 18-21, 2000, SIGPLAN Notices 35(9), pages 233--243. ACM, 2000. ISBN 1-58113-202-6.

Digital Library

[7]

Vincent Danos, Hugo Herbelin, and Laurent Regnier. Game semantics & abstract machines. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science (LICS '96), pages 394--405. IEEE Computer Society Press, 1996.

Digital Library

[8]

Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical Report 89/12, DIKU, University of Copenhagen, Copenhagen, Denmark, August 1989.

[9]

René David and Walter Py. λμ-calculus and Böhm's theorem. J. Symb. Log., 66(1):407--413, 2001.

[10]

Philippe de Groote. A CPS-translation of the λμ-calculus. In STison, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, CAAP'94, Edinburgh, U.K., April 11-13, 1994, volume 787 of Lecture Notes in Computer Science, pages 85--99. Springer-Verlag, 1994. ISBN 3-540-57879-X.

Digital Library

[11]

Kosta Došen and Zoran Petrić. The typed Böhm teorem. In Böhm theorem: applications to Computer Science Theory -- BOTH 2001 Crete, Greece, volume 50(2) of Electronic Notes in Theoretical Computer Science, page 13, 2001.

[12]

Matthias Felleisen. The theory and practice of first-class prompts. In Proceedings of the 15th ACM Symposium on Principles of Programming Languages (POPL '88), pages 180--190. ACM Press, New York, January 1988.

Digital Library

[13]

Matthias Felleisen and Daniel Friedman. Control operators, the secd machine, and the λ-calculus. In Formal description of programming concepts-III, pages 193--217. North-Holland, 1986.

[14]

Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, and Bruce F. Duba. Reasoning with continuations. In First Symposium on Logic and Computer Science, pages 131--141, 1986.

[15]

Andrzej Filinski. Representing monads. In Conf. Record 21st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL'94, Portland, OR, USA, 17-21 Jan. 1994, pages 446--457. ACM Press, New York, 1994.

Digital Library

[16]

Michael J. Fischer. λ-calculus schemata. In Proc. ACM Conference on Proving Assertions About Programs, volume 7(1) of SIGPLAN Notices, pages 104--109. ACM Press, New York, 1972.

Digital Library

[17]

Ken-etsu Fujita. A sound and complete cps-translation for λμ-calculus. In TLCA, pages 120--134, 2003.

Digital Library

[18]

Timothy G. Griffin. The formulae-as-types notion of control. In Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17-19 Jan 1990, pages 47--57. ACM Press, New York, 1990.

Digital Library

[19]

Thèrése Hardin, Luc Maranget, and Bruno Pagano. Functional back-ends within the lambda-sigma calculus. In ICFP, pages 25--33, 1996.

Digital Library

[20]

Hugo Herbelin. Explicit substitutions and reducibility. Journal of Logic and Computation, 11(3): 431--451, 2001.

[21]

Hugo Herbelin. C'est maintenant qu'on calcule: au cæ ur de la dualité. Habilitation à diriger les recherches, Université Paris 11, December 2005.

[22]

Hugo Herbelin. Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de λ-termes et comme calcul de stratégies gagnantes. Thése de doctorat, Université Paris 7, January 1995.

[23]

Hugo Herbelin. Games and weak-head reduction for classical PCF. In Philippe de Groote and JRoger Hindley, editors, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2-4, 1997, Proceedings, volume 1210 of Lecture Notes in Computer Science, pages 214--230. Springer, 1997. ISBN 3-540-62688-3.

Digital Library

[24]

Gregory F. Johnson. Gl -- a denotational testbed with continuations and partial continuations as first-class objects. In SIGPLAN '87: Papers of the Symposium on Interpreters and interpretive techniques, pages 165--176, New York, NY, USA, 1987. ACM Press. ISBN 0-89791-235-7. http://doi.acm.org/10.1145/29650.29668.

Digital Library

[25]

Gregory F. Johnson and Dominic Duggan. Stores and partial continuations as first-class objects in a language and its environment. In POPL, pages 158--168, 1988.

Digital Library

[26]

Thierry Joly. Codages, séparabilité et représentation de fonctions dans divers λ-calculs typés. Phd thesis, Université Paris 7, January 2000.

[27]

Yukiyoshi Kameyama and Masahito Hasegawa. A sound and complete axiomatization of delimited continuations. In Colin Runciman and Olin Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25--29, 2003, volume 38(9) of SIGPLAN Notices, pages 177--188. ACM Press, New York, 2003.

Digital Library

[28]

Yves Lafont, Bernhard Reus, and Thomas Streicher. Continuations semantics or expressing implication by negation. Technical Report 9321, Ludwig-Maximilians-Universität, München, 1993.

[29]

C.-H. Luke Ong. A semantic view of classical proofs: type-theoretic, categorical, denotational characterizations. In Proceedings of 11th IEEE Annual Symposium on Logic in Computer Science, pages 230--241. IEEE Computer Society Press, 1996.

Digital Library

[30]

C.-H. Luke Ong and Charles A. Stewart. A Curry-Howard foundation for functional computation with control. In Proceedings of ACM SIGPLAN--SIGACT Symposium on Principle of Programming Languages, Paris, January 1997, pages 215--227. ACM Press, 1997.

Digital Library

[31]

Luca Paolini. Call-by-Value separability and computability. In ARestivo and SRonchi della Rocca, editors, 7th Italian Conference Theoretical Computer Science, ICTCS'05, volume 2202 of Lecture Notes in Computer Science, pages 74--89. Springer-Verlag, 2001.

Digital Library

[32]

Michel Parigot. Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning: International Conference LPAR '92 Proceedings, St. Petersburg, Russia, pages 190--201. Springer-Verlag, 1992.

Digital Library

[33]

David Pym and Eike Ritter. On the semantics of classical disjunction. Journal of Pure and Applied Algebra, 159:315--338, 2001.

[34]

Amr Sabry. Note on axiomatizing the semantics of control operators. Technical Report CIS-TR-96-03, Dept of Information Science, Univ. of Oregon, 1996.

[35]

Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3--4): 289--360, 1993.

Digital Library

[36]

Alexis Saurin. Separation with streams in the λμ--calculus. In Proceedings, 20th Annual IEEE Symposium on Logic in Computer Science (LICS '05), pages 356--365. IEEE Computer Society Press, 2005.

Digital Library

[37]

Alexis Saurin. Typing streams in the λμ-calculus. In 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR '07), Lecture Notes in Artificial Intelligence. Springer-Verlag, 2007. to appear.

[38]

Peter Selinger. Control categories and duality: on the categorical semantics of the λμ-calculus. Mathematical Structures in Computer Science, 11 (2):207--260, 2001.

Digital Library

[39]

Chung-chieh Shan. Shift to control. In Olin Shivers and Oscar Waddell, editors, Proceedings of the 5th workshop on Scheme and Functional Programming, pages 99--107, 2004.

[40]

Alex K. Simpson. Categorical completeness results for simply typed lambda calculus. In MDezani-Ciancaglini and GPlotkin, editors, Typed Lambda Calculus and Applications TLCA'95, volume 902 of Lecture Notes in Computer Science, pages 414--427. Springer-Verlag, 1995.

Digital Library

[41]

Dorai Sitaram and Matthias Felleisen. Reasoning with continuations ii: full abstraction for models of control. In LFP '90: Proceedings of the 1990 ACM conference on LISP and functional programming, pages 161--175. ACM Press, 1990. ISBN 0-89791-368-X. http://doi.acm.org/10.1145/91556.91626.

Digital Library

[42]

Richard Statman. Completeness, invariance and λ-definability. J. Symb. Log., 47(1):17--26, 1982.

[43]

Philip Wadler. Call-by-value is dual to call-by-name. In Colin Runciman and Olin Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, volume 38(9) of SIGPLAN Notices, pages 189--201. ACM, 2003. ISBN 1-58113-756-7.

Digital Library

Cited By

Ostermann KBinder DSkupin ISüberkrüb TDownen P(2022)Introduction and elimination, left and rightProceedings of the ACM on Programming Languages10.1145/35476376:ICFP(438-465)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547637
Pédrot PHermanns HZhang LKobayashi NMiller D(2020)Russian Constructivism in a Prefascist TheoryProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394740(782-794)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394740
Miquey É(2019)A Classical Sequent Calculus with Dependent TypesACM Transactions on Programming Languages and Systems10.1145/323062541:2(1-47)Online publication date: 15-Mar-2019
https://dl.acm.org/doi/10.1145/3230625
Show More Cited By

Index Terms

An approach to call-by-name delimited continuations
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Control primitives

Recommendations

An approach to call-by-name delimited continuations
POPL '08

We show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al'...
A hierarchy for delimited continuations in call-by-name
FOSSACS'10: Proceedings of the 13th international conference on Foundations of Software Science and Computational Structures

Λμ-calculus was introduced as a Böhm-complete extension of Parigot's λμ-calculus. Λμ-calculus, contrarily to Parigot's calculus, is a calculus of CBN delimited control as evidenced by Herbelin and Ghilezan. In their seminal paper on (CBV) delimited ...
A proof-theoretic foundation of abortive continuations

We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce's law without enforcing Ex Falso Quodlibet. We show that a "natural" implementation of this logic is Parigot's classical natural ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2008

448 pages

ISBN:9781595936899

DOI:10.1145/1328438

General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

ACM SIGPLAN Notices Volume 43, Issue 1
POPL '08
January 2008
420 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1328897
Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL08

Sponsor:

POPL08: The 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 7 - 12, 2008

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
392
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)1

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ostermann KBinder DSkupin ISüberkrüb TDownen P(2022)Introduction and elimination, left and rightProceedings of the ACM on Programming Languages10.1145/35476376:ICFP(438-465)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547637
Pédrot PHermanns HZhang LKobayashi NMiller D(2020)Russian Constructivism in a Prefascist TheoryProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394740(782-794)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394740
Miquey É(2019)A Classical Sequent Calculus with Dependent TypesACM Transactions on Programming Languages and Systems10.1145/323062541:2(1-47)Online publication date: 15-Mar-2019
https://dl.acm.org/doi/10.1145/3230625
Cong YAsai K(2018)Handling delimited continuations with dependent typesProceedings of the ACM on Programming Languages10.1145/32367642:ICFP(1-31)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236764
JOHNSON-FREYD PDOWNEN PARIOLA Z(2017)Call-by-name extensionality and confluenceJournal of Functional Programming10.1017/S095679681700003X27Online publication date: 27-Feb-2017
https://doi.org/10.1017/S095679681700003X
DE'LIGUORO U(2015)The approximation theorem for the Λμ-calculusMathematical Structures in Computer Science10.1017/S096012951500028627:5(560-580)Online publication date: 28-Jul-2015
https://doi.org/10.1017/S0960129515000286
Downen PAriola Z(2014)Compositional semantics for composable continuationsACM SIGPLAN Notices10.1145/2692915.262814749:9(109-122)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628147
Downen PAriola ZJeuring JChakravarty M(2014)Compositional semantics for composable continuationsProceedings of the 19th ACM SIGPLAN international conference on Functional programming10.1145/2628136.2628147(109-122)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2628136.2628147
Munch-Maccagnoni GHenzinger TMiller D(2014)Formulae-as-types for an involutive negationProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603156(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603156
Tanaka AKameyama Y(2012)A call-by-name CPS hierarchyProceedings of the 11th international conference on Functional and Logic Programming10.1007/978-3-642-29822-6_21(260-274)Online publication date: 23-May-2012
https://dl.acm.org/doi/10.1007/978-3-642-29822-6_21
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents