A substructural type system for delimited continuations

Oleg Kiselyov, Chung Chieh Shan

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

19 Citations (Scopus)


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 directstyle program desugars it into continuation-passing style.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications - 8th International Conference,TLCA 2007, Proceedings
PublisherSpringer Verlag
Number of pages17
ISBN (Print)9783540732273
Publication statusPublished - 2007
Event8th International Conference on Typed Lambda Calculi and Applications,TLCA 2007 - Paris, France
Duration: 2007 Jun 262007 Jun 28

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4583 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference8th International Conference on Typed Lambda Calculi and Applications,TLCA 2007


Dive into the research topics of 'A substructural type system for delimited continuations'. Together they form a unique fingerprint.

Cite this