article

A type-theoretic foundation of delimited continuations

Authors:

Zena M. Ariola,

Amr SabryAuthors Info & Claims

Higher-Order and Symbolic Computation, Volume 22, Issue 3

Pages 233 - 273

https://doi.org/10.1007/s10990-007-9006-0

Published: 01 September 2009 Publication History

Abstract

There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters, the continuations become composable and the calculi become more expressive. We present a fine-grained analysis of control delimiters and formalise that their addition corresponds to the addition of a single dynamically-scoped variable modelling the special top-level continuation. From a type perspective, the dynamically-scoped variable requires effect annotations. In the presence of control, the dynamically-scoped variable can be interpreted in a purely functional way by applying a store-passing style. At the type level, the effect annotations are mapped within standard classical logic extended with the dual of implication, namely subtraction. A continuation-passing-style transformation of lambda-calculus with control and subtraction is defined. Combining the translations provides a decomposition of standard CPS transformations for delimited continuations. Incidentally, we also give a direct normalisation proof of the simply-typed lambda-calculus with control and subtraction.

References

[1]

Ariola, Z.M., Herbelin, H.: Minimal classical logic and control operators. In: Thirtieth International Colloquium on Automata, Languages and Programming, ICALP'03, Eindhoven, The Netherlands, June 30-July 4, 2003. Lecture Notes in Comput. Sci., vol. 2719, pp. 871-885. Springer, New York (2003).

Digital Library

[2]

Ariola, Z.M., Herbelin, H.: Control reduction theories: the benefit of structural substitution. J. Funct. Program. (2007, to appear).

[3]

Ariola, Z.M., Herbelin, H., Sabry, A.: A type-theoretic foundation of continuations and prompts. In: ACM SIGPLAN International Conference on Functional Programming, pp. 40-53. ACM Press, New York (2004).

[4]

Baba, K., Hirokawa, S., Fujita, K.: Parallel reduction in type free ?μ-calculus. Electron. Notes Theor. Comput. Sci. 42, 52-66 (2001).

[5]

Barbanera, F., Berardi, S.: Extracting constructive content from classical logic via control-like reductions. In: Bezem, M., Groote, J.F. (eds.) Proceedings 1st Intl. Conf. on Typed Lambda Calculi and Applications, TLCA'93, Utrecht, The Netherlands, 16-18 March 1993. Lecture Notes in Comput. Sci., vol. 664, pp. 45-59. Springer, Berlin (1993).

Digital Library

[6]

Crolard, T.: Subtractive logic. Theor. Comput. Sci. 254(1-2), 151-185 (2001).

[7]

Crolard, T.: A formulae-as-types interpretation of subtractive logic. J. Log. Comput. 14(4), 529-570 (2004) (Special issue on Modalities in Constructive Logics and Type Theories).

Digital Library

[8]

Curien, P.-L., Herbelin, H.: The duality of computation. In: ACM SIGPLAN International Conference on Functional Programming, pp. 233-243. ACM Press, New York (2000).

[9]

Danvy, O., Filinski, A.: A functional abstraction of typed contexts. Technical Report 89/12, DIKU, University of Copenhagen, Copenhagen, Denmark (1989).

[10]

Danvy, O., Filinski, A.: Abstracting control. In: Proceedings of the 1990 ACM Conference on LISP and Functional Programming, Nice, pp. 151-160. ACM Press, New York (1990).

Digital Library

[11]

David, R., Py, W.: Lambda-mu-calculus and Böhm's theorem. J. Symb. Log. 66(1), 407-413 (2001).

[12]

Dybvig, R.K., Peyton-Jones, S., Sabry, A.: A monadic framework for subcontinuations. J. Funct. Program. (2007, to appear). http://journals.cambridge.org/action/displayIssue?iid=168229.

[13]

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

Digital Library

[14]

Felleisen, M.: On the expressive power of programming languages. In: Jones, N. (ed.) ESOP '90 3rd European Symposium on Programming, Copenhagen, Denmark. Lecture Notes in Comput. Sci., vol. 432, pp. 134-151. Springer, New York (1990).

[15]

Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235-271 (1992).

[16]

Felleisen, M., Friedman, D., Kohlbecker, E.: A syntactic theory of sequential control. Theor. Comput. Sci. 52(3), 205-237 (1987).

Digital Library

[17]

Felleisen, M., Wand, M., Friedman, D.P., Duba, B.F.: Abstract continuations: a mathematical semantics for handling full functional jumps. In: Conference on LISP and Functional Programming, Snowbird, Utah, pp. 52-62. ACM Press, New York (1988).

[18]

Filinski, A.: Declarative continuations: an investigation of duality in programming language semantics. In: Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings. Lecture Notes in Comput. Sci., vol. 389, pp. 224-249. Springer, New York (1989).

[19]

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

[20]

Filinski, A.: Representing layered monads. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 175-188. ACM Press, New York (1999).

Digital Library

[21]

Fischer, M.J.: Lambda-calculus schemata. In: Proc. ACM Conference on Proving Assertions About Programs. SIGPLAN Notices, vol. 7(1), pp. 104-109. ACM Press, New York (1972).

[22]

Fischer, M.J.: Lambda-calculus schemata. Lisp Symb. Comput. 6(3/4), 259-288 (1993). http://www.brics.dk/~hosc/vol06/03-fischer.html. Earlier version available in the proceedings of an ACM Conference on Proving Assertions about Programs, SIGPLAN Notices, vol. 7, no. 1, January 1972.

Digital Library

[23]

Griffin, T.G.: 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, pp. 47-57. ACM Press, New York (1990).

[24]

Gunter, C.A., Rémy, D., Riecke, J.G.: A generalization of exceptions and control in ML-like languages. In: Functional Programming & Computer Architecture. ACM Press, New York (1995).

[25]

Guzmán, J., Suárez, A.: An extended type system for exceptions. In: Record of the fifth ACM SIGPLAN workshop on ML and its Applications. Also appeared as Research Report 2265, INRIA, BP 105-78153, Le Chesnay Cedex, France (1994).

[26]

Haynes, C.T.: Logic continuations. In: Proceedings of the Third International Conference on Logic Programming. Lecture Notes in Comput. Sci., vol. 225, pp. 671-685. Springer, Berlin (1986).

[27]

Haynes, C.T., Friedman, D., Wand, M.: Obtaining coroutines from continuations. J. Comput. Lang. 11, 143-153 (1986).

Digital Library

[28]

Herbelin, H.: Explicit substitutions and reducibility. J. Log. Comput. 11(3), 431-451 (2001).

[29]

Hieb, R., Dybvig, R.K.: Continuations and concurrency. In: PPoPP '90, Symposium on Principles and Practice of Parallel Programming, Seattle, Washington, March 14-16. SIGPLAN Notices, vol. 25(3), pp. 128-136. ACM Press, New York (1990).

[30]

Hieb, R., Dybvig, K., Anderson, C.W. III: Subcontinuations. Lisp Symb. Comput. 7(1), 83-110 (1994).

Digital Library

[31]

Hofmann, M.: Sound and complete axiomatisations of call-by-balue control operators. Math. Struct. Comput. Sci. 5(4), 461-482 (1995).

[32]

Howard, W.: The formulae-as-types notion of construction. In: Hindley, J.R., Seldin, J.P. (eds.) To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pp. 479-490. Academic, New York (1980).

[33]

Kameyama, Y.: A type-theoretic study on partial continuations. In: IFIP TCS, pp. 489-504 (2000).

Digital Library

[34]

Kameyama, Y.: Towards logical understanding of delimited continuations. In: Proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW'01) (2001).

[35]

Kameyama, Y., Hasegawa, M.: A sound and complete axiomatization of delimited continuations. In: Proc. of 8th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP'03, Uppsala, Sweden, 25-29 Aug. 2003. SIGPLAN Notices, vol. 38(9), pp. 177-188. ACM Press, New York (2003).

[36]

Lillibridge, M.: Unchecked exceptions can be strictly more powerful than Call/CC. Higher-Order Symb. Comput. 12(1), 75-104 (1999).

Digital Library

[37]

Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pp. 14-23. IEEE Press (1989).

[38]

Moreau, L.: A syntactic theory of dynamic binding. Higher-Order Symb. Comput. 11(3), 233-279 (1998).

Digital Library

[39]

Moreau, L., Queinnec, C.: Partial continuations as the difference of continuations. A duumvirate of control operators. In: International Conference on Programming Language Implementation and Logic Programming (PLILP'94), Madrid, Spain, pp. 182-197. Springer, Berlin (1994).

[40]

Murthy, C.: Control operators, hierarchies, and pseudo-classical type systems: a--translation at work. In: ACM workshop on Continuations, pp. 49-71 (1992).

[41]

Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: Conf. Record 24th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL'97, Paris, France, 15-17 Jan. 1997, pp. 215-227. ACM Press, New York (1997).

[42]

Parigot, M.: Lambda-mu-calculus: an algorithmic interpretation of classical natural deduction. In: Logic Programming and Automated Reasoning: International Conference LPAR '92 Proceedings, St. Petersburg, Russia, pp. 190-201. Springer, Berlin (1992).

Digital Library

[43]

Rauszer, C.: Semi-boolean algebras and their application to intuitionistic logic with dual connectives. Fundam. Math. 83, 219-249 (1974).

[44]

Riecke, J.G., Thielecke, H.: Typed exceptions and continuations cannot macro-express each other. In: Proceedings of the 26th International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Comput. Sci., vol. 1644, pp. 635-644. Springer, Berlin (1999).

[45]

Shan, C.: Shift to control. In: Shivers, O.,Waddell, O. (eds.) Proceedings of the 5thWorkshop on Scheme and Functional Programming, pp. 99-107. Technical report, Computer Science Department, Indiana University (2004).

[46]

Sitaram, D., Felleisen, M.: Control delimiters and their hierarchies. Lisp Symb. Comput. 3(1), 67-99 (1990a).

Digital Library

[47]

Sitaram, D., Felleisen, M.: Reasoning with continuations II: full abstraction for models of control. In: LFP '90: Proceedings of the 1990 ACMConference on LISP and Functional Programming, pp. 161-175. ACM Press, New York (1990b).

Digital Library

[48]

Thielecke, H.: On exceptions versus continuations in the presence of state. In: Proceedings of the Ninth European Symposium On Programming (ESOP). Lecture Notes in Comput. Sci., vol. 1782, pp. 397-411. Springer, Berlin (2000).

[49]

Thielecke, H.: Contrasting exceptions and continuations. Available from http://www.cs.bham.ac.uk/~hxt/research/exncontjournal.pdf (2001).

[50]

Thielecke, H.: Comparing control constructs by double-barrelled CPS. Higher-Order Symb. Comput. 15(2/3), 119-136 (2002).

[51]

Wadler, P.: Monads and composable continuations. Lisp Symb. Comput. 7(1), 39-56 (1994).

Digital Library

[52]

Wand, M.: Continuation-based multiprocessing. Higher-Order Symb. Comput. 12(3), 285-299 (1999), http://www.brics.dk/~hosc/vol12/3-wand.html. Reprinted from the Proceedings of the 1980 Lisp Conference, with a foreword

Digital Library

Cited By

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
Miquey É(2017)A Classical Sequent Calculus with Dependent TypesProgramming Languages and Systems10.1007/978-3-662-54434-1_29(777-803)Online publication date: 25-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54434-1_29
Show More Cited By

A type-theoretic foundation of delimited continuations
1. Theory of computation

Recommendations

A type-theoretic foundation of continuations and prompts
ICFP '04

There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters (prompts), the continuations become composable and the calculi are believed to become more ...
A type-theoretic foundation of continuations and prompts
ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming

There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters (prompts), the continuations become composable and the calculi are believed to become more ...
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 Higher-Order and Symbolic Computation

Higher-Order and Symbolic Computation Volume 22, Issue 3

September 2009

92 pages

ISSN:1388-3690

Issue’s Table of Contents

Copyright © Copyright © 2010 Springer Science+Business Media, LLC.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 September 2009

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Miquey É(2017)A Classical Sequent Calculus with Dependent TypesProgramming Languages and Systems10.1007/978-3-662-54434-1_29(777-803)Online publication date: 25-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54434-1_29
Liang CMiller D(2015)On Subexponentials, Synthetic Connectives, andźMulti-level Delimited ControlProceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Volume 945010.1007/978-3-662-48899-7_21(297-312)Online publication date: 24-Nov-2015
https://dl.acm.org/doi/10.1007/978-3-662-48899-7_21
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
Kammar OLindley SOury N(2013)Handlers in actionACM SIGPLAN Notices10.1145/2544174.250059048:9(145-158)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2544174.2500590
Kammar OLindley SOury NMorrisett GUustalu T(2013)Handlers in actionProceedings of the 18th ACM SIGPLAN international conference on Functional programming10.1145/2500365.2500590(145-158)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2500365.2500590
Downen PAriola Z(2012)A systematic approach to delimited control with multiple promptsProceedings of the 21st European conference on Programming Languages and Systems10.1007/978-3-642-28869-2_12(234-253)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28869-2_12
Show More Cited By

View Options

View options

Get Access

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

Media

Figures

Other

Tables

View Issue’s Table of Contents