More Web Proxy on the site http://driver.im/

Article

From control effects to typed continuation passing

Author:

Hayo ThieleckeAuthors Info & Claims

POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 139 - 149

https://doi.org/10.1145/604131.604144

Published: 15 January 2003 Publication History

Abstract

First-class continuations are a powerful computational effect, allowing the programmer to express any form of jumping. Types and effect systems can be used to reason about continuations, both in the source language and in the target language of the continuation-passing transform. In this paper, we establish the connection between an effect system for first-class continuations and typed versions of continuation-passing style. A region in the effect system determines a local answer type for continuations, such that the continuation transforms of pure expressions are parametrically polymorphic in their answer types. We use this polymorphism to derive transforms that make use of effect information, in particular, a mixed linear/non-linear continuation-passing transform, in which expressions without control effects are passed their continuations linearly.

References

[1]

Amal Ahmed and David Walker. The logical approach to stack typing. ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'03), 2003.]]

Digital Library

[2]

Andrew Appel. Compiling with Continuations. Cambridge University Press, 1992.]]

Digital Library

[3]

Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Region analysis and the polymorphic lambda calculus. In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science, pages 88--97, 1999.]]

Digital Library

[4]

Josh Berdine, Peter W. O'Hearn, Uday Reddy, and Hayo Thielecke. Linear continuation passing. Higher-order and Symbolic Computation, 15(2/3), 2002.]]

Digital Library

[5]

Carl Bruggeman, Oscar Waddell, and R. Kent Dybvig. Representing control in the presence of one-shot continuations. ACM SIGPLAN Notices, 31(5):99--107, May 1996.]]

Digital Library

[6]

Olivier Danvy. Formalizing implementation strategies for first-class continuations. In Gert Smolka, editor, Programming Languages and Systems, 9th European Symposium on Programming, ESOP, number 1782 in LNCS, pages 88--103. Springer Verlag, 2000.]]

Digital Library

[7]

Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361--391, December 1992.]]

[8]

Olivier Danvy and Lasse R. Nielsen. A first-order one-pass CPS transformation. In Foundations of Software Science and Computation Structures (FoSSaCS) '02, number 2303 in LNCS. Springer, 2002.]]

Digital Library

[9]

Bruce Duba, Robert Harper, and David MacQueen. Typing first-class continuations in ML. In Principles of Programming Languages (POPL'91), pages 163--173. ACM, January 1991.]]

Digital Library

[10]

Matthias Felleisen. The theory and practice of first-class prompts. In Principles of Programming Languages (POPL '88), pages 180--190. ACM, January 1988.]]

Digital Library

[11]

Carsten Führmann. Varieties of effects. In Foundations of Software Science and Computation Structures (FOSSACS) 2002, volume 2303 of LNCS, pages 144--158. Springer, 2002.]]

[12]

Timothy G. Griffin. A formulae-as-types notion of control. In Principles of Programming Languages (POPL '90), pages 47--58. ACM, 1990.]]

Digital Library

[13]

Robert Harper and Mark Lillibridge. Polymorphic type assignment and CPS conversion. In Olivier Danvy and Carolyn Talcott, editors, Proceedings of the ACM SIGPLAN Workshop on Continuations CW'92, pages 13--22. Department of Computer Science, Stanford University, June 1992. Published as technical report STAN--CS--92--1426.]]

[14]

Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Principles of Programming Languages (POPL '93), pages 206--219. ACM, 1993.]]

Digital Library

[15]

Pierre Jouvelot and David K. Gifford. Reasoning about continuations with control effects. In Prgramming Language Design and Implementation (PLDI), pages 218--226. ACM, 1988.]]

Digital Library

[16]

Richard Kelsey, William Clinger, and Jonathan Rees, editors. Revised5 report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(1):7--105, 1998.]]

Digital Library

[17]

John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Principles of Programming Languages (POPL '88), pages 47--57. ACM, 1988.]]

Digital Library

[18]

Saunders Mac Lane. Categories for the Working Mathematician. Springer Verlag, 1971.]]

[19]

Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi (summary). In Rohit Parikh, editor, Logics of Programs, number 193 in Lecture Notes in Computer Science, pages 219--224. Springer-Verlag, 1985.]]

Digital Library

[20]

Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.]]

Digital Library

[21]

Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. In Principles of Programming Languages (POPL '98), pages 85--97. ACM, 1998.]]

Digital Library

[22]

Lasse R. Nielsen. A selective CPS transformation. In 27th Annual Conference on the Mathematical Foundations of Programming Semantics (MFPS), number 45 in ENTCS. Elsevier, 2001.]]

[23]

Andrew M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, 10:321--359, 2000.]]

Digital Library

[24]

John C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513--523, Amsterdam, 1983. Elsevier Science Publishers B. V. (North-Holland).]]

[25]

Jon G. Riecke and Hayo Thielecke. Typed exceptions and continuations cannot macro-express each other. In Proceedings 26th International Colloquium on Automata, Languages and Programming (ICALP), volume 1644 of LNCS, pages 635--644. Springer Verlag, 1999.]]

[26]

Guy Steele. Rabbit: A compiler for Scheme. Technical Report AI TR 474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, May 1978.]]

Digital Library

[27]

Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value lambda-calculus using a stack of regions. In Principles of Programming Languages (POPL '94), pages 88--201. ACM, 1994.]]

Digital Library

[28]

Philip Wadler. Theorems for free! In 4th International Conference on Functional Programming and Computer Architecture (FPCA'89), pages 347--359. ACM, 1989.]]

Digital Library

Cited By

Kawamata FUnno HSekiyama TTerauchi T(2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633280
Müller MSchuster PStarup JOstermann KBrachthäuser J(2023)From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228317:OOPSLA2(941-970)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622831
Schuster PBrachthäuser JMüller MOstermann KJhala RDillig I(2022)A typed continuation-passing translation for lexical effect handlersProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523710(566-579)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523710
Show More Cited By

Index Terms

From control effects to typed continuation passing
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
    2. General programming languages
      1. Language features
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

Compiling effect handlers in capability-passing style

Effect handlers encourage programmers to abstract over repeated patterns of complex control flow. As of today, this abstraction comes at a significant price in performance. In this paper, we aim to achieve abstraction without regret for effect handlers.
...
From control effects to typed continuation passing

First-class continuations are a powerful computational effect, allowing the programmer to express any form of jumping. Types and effect systems can be used to reason about continuations, both in the source language and in the target language of the ...
On the power of coercion abstraction
POPL '12

Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2003

308 pages

ISBN:1581136285

DOI:10.1145/604131

General Chair:
Alex Aiken
University of California, Berkeley, CA
,
Program Chair:
Greg Morrisett
Cornell University

ACM SIGPLAN Notices Volume 38, Issue 1
January 2003
298 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/640128
Issue’s Table of Contents

Copyright © 2003 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: 15 January 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL03

Sponsor:

POPL03: POPL '03 - The 30th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 15 - 17, 2003

Louisiana, New Orleans, USA

Acceptance Rates

POPL '03 Paper Acceptance Rate 24 of 126 submissions, 19%;

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

47
Total Citations
View Citations
555
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)2

Reflects downloads up to 23 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kawamata FUnno HSekiyama TTerauchi T(2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633280
Müller MSchuster PStarup JOstermann KBrachthäuser J(2023)From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228317:OOPSLA2(941-970)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622831
Schuster PBrachthäuser JMüller MOstermann KJhala RDillig I(2022)A typed continuation-passing translation for lexical effect handlersProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523710(566-579)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523710
Schuster PBrachthäuser JOstermann K(2022)Region-based Resource Management and Lexical Exception Handlers in Continuation-Passing StyleProgramming Languages and Systems10.1007/978-3-030-99336-8_18(492-519)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_18
Im H(2021)On Correspondence between Selective CPS Transformation and Selective Double Negation TranslationMathematics10.3390/math90403859:4(385)Online publication date: 15-Feb-2021
https://doi.org/10.3390/math9040385
Narayanan PShan C(2020)Symbolic Disintegration with a Variety of Base MeasuresACM Transactions on Programming Languages and Systems10.1145/337420842:2(1-60)Online publication date: 19-May-2020
https://dl.acm.org/doi/10.1145/3374208
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
Asai KUehara C(2018)Selective CPS transformation for shift and resetProceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation - PEPM '1810.1145/3175493.3162069(40-52)Online publication date: 2018
https://doi.org/10.1145/3175493.3162069
Asai KUehara CHenglein FKo H(2017)Selective CPS transformation for shift and resetProceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3162069(40-52)Online publication date: 25-Dec-2017
https://dl.acm.org/doi/10.1145/3162069
Bowman WCong YRioux NAhmed A(2017)Type-preserving CPS translation of Σ and Π types is not not possibleProceedings of the ACM on Programming Languages10.1145/31581102:POPL(1-33)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158110
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