2 Search Results for "Cong, Youyou"

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-dev.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}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.16
Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators

Authors: Maika Fujii and Kenichi Asai

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

Abstract
This paper derives an abstract machine and a virtual machine for the λ-calculus with four variants of delimited-control operators: shift/reset, control/prompt, shift₀/reset₀, and control₀/prompt₀. Starting from Shan’s definitional interpreter for the four operators, we successively apply various meaning-preserving transformations. Both trails of invocation contexts (needed for control and control₀) and metacontinuations (needed for shift₀ and control₀) are defunctionalized and eventually represented as a list of stack frames. The resulting virtual machine clearly models not only how the control operators and captured continuations behave but also when and which portion of stack frames is copied to the heap.
Cite as

Maika Fujii and Kenichi Asai. Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{fujii_et_al:LIPIcs.FSCD.2021.16,
  author =	{Fujii, Maika and Asai, Kenichi},
  title =	{{Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{16:1--16:19},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.16},
  URN =		{urn:nbn:de:0030-drops-142547},
  doi =		{10.4230/LIPIcs.FSCD.2021.16},
  annote =	{Keywords: delimited-control operators, functional derivation, CPS transformation, defunctionalization, abstract machine, virtual machine}
}
  • Refine by Author
  • 2 Asai, Kenichi
  • 1 Cong, Youyou
  • 1 Fujii, Maika
  • 1 Honda, Kaho
  • 1 Ishio, Chiaki

  • Refine by Classification
  • 2 Theory of computation → Control primitives
  • 1 Software and its engineering → Virtual machines
  • 1 Theory of computation → Abstract machines
  • 1 Theory of computation → Functional constructs
  • 1 Theory of computation → Lambda calculus
  • Show More...

  • Refine by Keyword
  • 1 CPS transformation
  • 1 CPS translation
  • 1 abstract machine
  • 1 control and prompt
  • 1 control operators
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 2 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact