DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2021.12

A Functional Abstraction of Typed Invocation Contexts

Authors: Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract

In their paper "A Functional Abstraction of Typed Contexts", Danvy and Filinski show how to derive a type system of the shift and reset operators from a CPS translation. In this paper, we show how this method scales to Felleisen’s control and prompt operators. Compared to shift and reset, control and prompt exhibit a more dynamic behavior, in that they can manipulate a trail of contexts surrounding the invocation of captured continuations. Our key observation is that, by adopting a functional representation of trails in the CPS translation, we can derive a type system that allows fine-grain reasoning of programs involving manipulation of invocation contexts.

Cite as

Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai. A Functional Abstraction of Typed Invocation Contexts. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{cong_et_al:LIPIcs.FSCD.2021.12,
  author =	{Cong, Youyou and Ishio, Chiaki and Honda, Kaho and Asai, Kenichi},
  title =	{{A Functional Abstraction of Typed Invocation Contexts}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{12:1--12:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.12},
  URN =		{urn:nbn:de:0030-drops-142507},
  doi =		{10.4230/LIPIcs.FSCD.2021.12},
  annote =	{Keywords: delimited continuations, control operators, control and prompt, CPS translation, type system}
}

Search Results

Documents authored by Honda, Kaho

A Functional Abstraction of Typed Invocation Contexts

Abstract

Cite as

Thanks for your feedback!

Could not send message