A substructural type system for delimited continuations

Oleg Kiselyov, Chung Chieh Shan

研究成果: Conference contribution

14 被引用数 (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.

本文言語English
ホスト出版物のタイトルTyped Lambda Calculi and Applications - 8th International Conference,TLCA 2007, Proceedings
ページ223-239
ページ数17
出版ステータスPublished - 2007 12 1
外部発表はい
イベント8th International Conference on Typed Lambda Calculi and Applications,TLCA 2007 - Paris, France
継続期間: 2007 6 262007 6 28

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
4583 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

Other8th International Conference on Typed Lambda Calculi and Applications,TLCA 2007
国/地域France
CityParis
Period07/6/2607/6/28

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「A substructural type system for delimited continuations」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル