Abstract
We propose type systems that abstractly interpret small-step rather than big-step operational semantics. We treat an expression or evaluation context as a structure in a linear logic with hypothetical reasoning. Evaluation order is not only regulated by familiar focusing rules in the operational semantics, but also expressed by structural rules in the type system, so the types track control flow more closely. Binding and evaluation contexts are related, but the latter are linear.
We use these ideas to build a type system for delimited continuations. It lets control operators change the answer type or act beyond the nearest dynamically-enclosing delimiter, yet needs no extra fields in judgments and arrow types to record answer types. The typing derivation of a direct-style program desugars it into continuation-passing style.
Thanks to Olivier Danvy, Andrzej Filinski, Michael Stone, Philip Wadler, and the anonymous referees. The appendices to this paper are online at http://okmij.org/ftp/papers/delim-control-logic.pdf
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ager, M.S., Biernacki, D., Danvy, O., Midtgaard, J.: A functional correspondence between evaluators and abstract machines. In: Proc. 5th intl. conf. principles & practice of declarative prog. pp. 8–19 (2003)
Ager, M.S., Danvy, O., Midtgaard, J.: A functional correspondence between call-by-need evaluators and lazy abstract machines. Info. Proc. Lett. 90(5), 223–232 (2004)
Ager, M.S., Danvy, O., Midtgaard, J.: A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theor. Comp. Sci. 342(1), 149–172 (2005)
Ariola, Z.M., Herbelin, H., Sabry, A.: A type-theoretic foundation of continuations and prompts. In: ICFP, pp. 40–53 (2004)
Atkey, R.: Parameterised notions of computation. In: MSFP 2006. Conor McBride and Tarmo Uustalu. Electronic Workshops in Computing. Electronic Workshops in Computing, British Computer Society, Vancouver (2006)
Balat, V., Danvy, O.: Memoization in type-directed partial evaluation. In: Batory, D., Consel, C., Taha, W. (eds.) GPCE 2002. LNCS, vol. 2487, pp. 78–92. Springer, Heidelberg (2002)
Balat, V., Di Cosmo, R., Fiore, M.: Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In: POPL, pp. 64–76 (2004)
Barker, C.: Direct compositionality on demand. In: Barker, C., Jacobson, P. (eds.) Direct compositionality, pp. 102–131. Oxford University Press, New York (2007)
Barker, C., Shan, C.-c.: Types as graphs: Continuations in type logical grammar. J. Logic, Lang. & Info. 15(4), 331–370 (2006)
Biernacka, M., Biernacki, D., Danvy, O.: An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Comp. Sci. 1(2:5) (2005)
Biernacka, M., Danvy, O.: A syntactic correspondence between context-sensitive calculi and abstract machines. Theor. Comp. Sci. 375(1-3), 76–108 (2007)
Biernacki, D., Danvy, O.: From interpreter to logic engine by defunctionalization. In: Bruynooghe, M. (ed.) LOPSTR 2003. LNCS, vol. 3018, pp. 143–159. Springer, Heidelberg (2004)
Cousot, P.: Types as abstract interpretations. In POPL, pp. 316–331 (1997)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pp. 238–252 (1977)
Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP, pp. 233–243 (2000)
Danvy, O.: Type-directed partial evaluation. In: POPL, pp. 242–257 (1996)
Danvy, O., Filinski, A.: A functional abstraction of typed contexts. Tech. Rep. 89/12, DIKU (1989) http://www.daimi.au.dk/~danvy/Papers/fatc.ps.gz
Danvy, O.: Abstracting control. In: Proc. conf. Lisp & funct. prog. pp. 151–160 (1990)
Danvy, O.: Representing control: A study of the CPS transformation. Math. Structures Comp. Sci. 2(4), 361–391 (1992)
Danvy, O., Nielsen, L.R.: Syntactic theories in practice. In: van den Brand, M., Verma, R. (eds.) RULE 2001: 2nd intl. workshop on rule-based prog. Electron. Notes in Theor. Comp. Sci, vol. 59(4), pp. 358–374. Elsevier, Amsterdam (2001)
Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Report RS-04-26, BRICS (2004)
Dunfield, J., Pfenning, F.: Tridirectional typechecking. In: POPL, pp. 281–292 (2004)
Dybjer, P., Filinski, A.: Normalization and partial evaluation. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 137–192. Springer, Heidelberg (2002)
Dybvig, R.K., Peyton Jones, S.L., Sabry, A.: A monadic framework for delimited continuations. Tech. Rep. 615, Indiana U (2005)
Felleisen, M.: The calculi of λ υ -CS conversion: A syntactic theory of control and state in imperative higher-order programming languages. Ph.D. thesis, Indiana U. (1987)
Felleisen, M.: The theory and practice of first-class prompts. In: POPL, pp. 180–190 (1988)
Felleisen, M., Flatt, M.: Programming languages and lambda calculi (2006), http://www.cs.utah.edu/plt/publications/pllc.pdf
Felleisen, M., Friedman, D.P.: Control operators, the SECD machine, and the λ-calculus. In: Wirsing, M. (ed.) Formal description of prog. concepts III, pp. 193–217. Elsevier, Amsterdam (1987)
Filinski, A.: Declarative continuations: An investigation of duality in programming language semantics. In: Pitt, D.H., Rydeheard, D.E., Dybjer, P., Pitts, A.M., Poigné, A. (eds.) Category Theory and Computer Science. LNCS, vol. 389, pp. 224–249. Springer, Heidelberg (1989)
Filinski, A.: Representing monads. In: POPL, pp. 446–457 (1994)
Filinski, A.: Controlling effects. Ph.D. thesis, CMU (1996)
Filinski, A.: Representing layered monads. In: POPL, pp. 175–188 (1999)
Filinski, A.: Normalization by evaluation for the computational lambda-calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 151–165. Springer, Heidelberg (2001)
Gifford, D.K., Lucassen, J.M.: Integrating functional and imperative programming. In: Proc. conf. Lisp & funct. prog. pp. 28–38 (1986)
Graunke, P.T.: Web interactions. Ph.D. thesis, Northeastern U (2003)
Griffin, T.G.: A formulae-as-types notion of control. In: POPL, pp. 47–58 (1990)
Grobauer, B., Yang, Z.: The second Futamura projection for type-directed partial evaluation. Higher-Order & Symbolic Comp. 14(2-3), 173–219 (2001)
Gunter, C.A., Rémy, D., Riecke, J.G.: A generalization of exceptions and control in ML-like languages. In: Peyton Jones, S.L. (ed.) Funct. prog. lang. & comp. architecture: 7th conf. pp. 12–23 (1995)
Gunter, C.A., Rémy, D., Riecke, J.G.: Return types for functional continuations (1998), http://pauillac.inria.fr/~remy/work/ cupto/
Hieb, R., Dybvig, R.K.: Continuations and concurrency. In: Proc. 2nd symposium on principles & practice of parallel prog. pp. 128–136 (1990)
Huet, G.: The zipper. J. Funct. Prog. 7(5), 549–554 (1997)
Kameyama, Y.: Towards logical understanding of delimited continuations. In: Amr, S. (ed.) Proc. 3rd workshop on continuations, pp. 27–33. Tech. Rep. 545, Indiana U (2001)
Kiselyov, O.: How to remove a dynamic prompt: Static and dynamic delimited continuation operators are equally expressible. Tech. Rep. 611, Indiana U (2005)
Kiselyov, O., Shan, C.-c., Friedman, D.P., Sabry, A.: Backtracking, interleaving, and terminating monad transformers (functional pearl). In: ICFP, pp. 192–203 (2005)
Kiselyov, O., Shan, C.-c., Sabry, A.: Delimited dynamic binding. In: ICFP, pp. 26–37 (2006)
Lambek, J.: The mathematics of sentence structure. Amer. Math. Monthly 65(3), 154–170 (1958)
Lawall, J.L., Danvy, O.: Continuation-based partial evaluation. In: Proc. conf. Lisp & funct. prog. pp. 227–238 (1994)
Lucassen, J.M.: Types and effects: Towards the integration of functional and imperative programming. Ph.D. thesis, MIT (1987)
Moortgat, M.: Categorial type logics. In: van Benthem, J.F.A.K., ter Meulen, A.G.B. (eds.) Handbook of logic and language, ch. 2, Elsevier, Amsterdam (1997)
Murphy, T., Crary, K., Harper, R.: Distributed control ow with classical modal logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 51–69. Springer, Heidelberg (2005)
Murthy, C.R.: Control operators, hierarchies, and pseudo-classical type systems: A-translation at work. In: Danvy, O., Talcott, C. (eds.) Proc. workshop on continuations, pp. 49–71 (1992) Tech. Rep. STAN-CS-92-1426, Stanford U.
Polakow, J.: Ordered linear logic and applications. Ph.D. thesis, CMU (2001)
Queinnec, C.: Continuations and web servers. Higher-Order & Symbolic Comp. 17(4), 277–295 (2004)
Restall, G.: An introduction to substructural logics. Routledge, London (2000)
Selinger, P.: Control categories and duality: On the categorical semantics of the lambda-mu calculus. Math. Structures Comp. Sci. 11, 207–260 (2001)
Sewell, P., Leifer, J.J., Wansbrough, K., Nardelli, F.Z., Allen-Williams, M., Habouzit, P., Vafeiadis, V.: Acute: High-level programming language design for distributed computation. In: ICFP, pp. 15–26 (2005)
Shan, C.-c.: Shift to control. In: Shivers, O., Waddell, O. (eds.) Proc. Scheme workshop, pp. 99–107, Tech. Rep. 600, Indiana U. (2004)
Shan, C.-c.: Linguistic side effects. Ph.D. thesis, Harvard U. (2005)
Sitaram, D.: Handling control. In: PLDI, pp. 147–155 (1993)
Sumii, E.: An implementation of transparent migration on standard Scheme. In: Felleisen, M. (ed.) Proc. Scheme workshop, pp. 61–63, Tech. Rep. 00-368, Rice U (2000)
Talpin, J.-P., Jouvelot, P.: Polymorphic type, region and effect inference. J. Funct. Prog. 2(3), 245–271 (1992)
Talpin, J.-P., Jouvelot, P.: The type and effect discipline. Info. & Comp. 111(2), 245–296 (1994)
Thielecke, H.: From control effects to typed continuation passing. In: POPL, pp. 139–149 (2003)
Thiemann, P.: Combinators for program generation. J. Funct. Prog. 9(5), 483–525 (1999)
Wadler, P.L.: The marriage of effects and monads. In: ICFP, pp. 63–74 (1998)
Wadler, P.L.: Call-by-value is dual to call-by-name. In: ICFP (2003)
Wand, M., Friedman, D.P.: The mystery of the tower revealed: A non-reflective description of the reflective tower. Lisp & Symbolic Comp. 1(1), 11–37 (1988)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Info. & Comp. 115(1), 38–94 (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Kiselyov, O., Shan, Cc. (2007). A Substructural Type System for Delimited Continuations. In: Della Rocca, S.R. (eds) Typed Lambda Calculi and Applications. TLCA 2007. Lecture Notes in Computer Science, vol 4583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73228-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-73228-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73227-3
Online ISBN: 978-3-540-73228-0
eBook Packages: Computer ScienceComputer Science (R0)