3 Search Results for "Muroya, Koko"

Document
Early Ideas
DOI: 10.4230/LIPIcs.CALCO.2021.21
Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas)

Authors: Koko Muroya, Takahiro Sanada, and Natsuki Urabe

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
We describe our ongoing work on generalizing some quantitatively constrained notions of weak simulation up-to that are recently introduced for deterministic systems modeling program execution. We present and discuss a new notion dubbed preorder-constrained simulation that allows comparison between words using a preorder, instead of equality.
Cite as

Koko Muroya, Takahiro Sanada, and Natsuki Urabe. Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{muroya_et_al:LIPIcs.CALCO.2021.21,
  author =	{Muroya, Koko and Sanada, Takahiro and Urabe, Natsuki},
  title =	{{Preorder-Constrained Simulation for Nondeterministic Automata}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{21:1--21:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.21},
  URN =		{urn:nbn:de:0030-drops-153762},
  doi =		{10.4230/LIPIcs.CALCO.2021.21},
  annote =	{Keywords: simulation, weak simulation, up-to technique, language inclusion, preorder}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.32
The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter

Authors: Koko Muroya and Dan R. Ghica

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
Girard's Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been also successfully applied to programming languages. One way is to use abstract machines that pass a token in a fixed graph, along a path indicated by the GoI. These token-passing abstract machines are space efficient, because they handle duplicated computation by repeating the same moves of a token on the fixed graph. Although they can be adapted to obtain sound models with regard to the equational theories of various evaluation strategies for the lambda calculus, it can be at the expense of significant time costs. In this paper we show a token-passing abstract machine that can implement evaluation strategies for the lambda calculus, with certified time efficiency. Our abstract machine, called the Dynamic GoI Machine (DGoIM), rewrites the graph to avoid replicating computation, using the token to find the redexes. The flexibility of interleaving token transitions and graph rewriting allows the DGoIM to balance the trade-off of space and time costs. This paper shows that the DGoIM can implement call-by-need evaluation for the lambda calculus by using a strategy of interleaving token passing with as much graph rewriting as possible. Our quantitative analysis confirms that the DGoIM with this strategy of interleaving the two kinds of possible operations on graphs can be classified as “efficient” following Accattoli’s taxonomy of abstract machines.
Cite as

Koko Muroya and Dan R. Ghica. The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{muroya_et_al:LIPIcs.CSL.2017.32,
  author =	{Muroya, Koko and Ghica, Dan R.},
  title =	{{The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{32:1--32:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.32},
  URN =		{urn:nbn:de:0030-drops-76886},
  doi =		{10.4230/LIPIcs.CSL.2017.32},
  annote =	{Keywords: Geometry of Interaction, cost analysis, call-by-need reduction}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.2
Coalgebras and Higher-Order Computation: a GoI Approach

Authors: Ichiro Hasuo

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Girard's geometry of interaction (GoI) can be seen---in one practical aspect of it---as a compositional compilation method from functional programs to sequential machines. There tokens move around and express interactions between (parts of) programs. Intrigued by the combination of abstract structures and concrete dynamics in GoI, our line of work has aimed at exploiting, in GoI, results from the theory of coalgebra---a categorical abstraction of state-based transition systems that has found its use principally in concurrency theory. Such reinforced connection between higher-order computation and state-based dynamics is made possible thanks to an elegant categorical axiomatization of GoI by Abramsky, Haghverdi and Scott, where traced monoidal categories are identified to be the essential structure behind. In the talk I shall lay out these basic ideas, together with some of our results on: GoI semantics for a quantum programming language; and our ``memoryful'' extension of GoI with algebraic effects. The talk is based on my joint work with my colleague Naohiko Hoshino (RIMS, Kyoto Univer- sity) and my (former) students Koko Muroya (University of Birmingham) and Toshiki Kataoka (University of Tokyo), to whom I owe special thanks.
Cite as

Ichiro Hasuo. Coalgebras and Higher-Order Computation: a GoI Approach. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{hasuo:LIPIcs.FSCD.2016.2,
  author =	{Hasuo, Ichiro},
  title =	{{Coalgebras and Higher-Order Computation: a GoI Approach}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.2},
  URN =		{urn:nbn:de:0030-drops-59698},
  doi =		{10.4230/LIPIcs.FSCD.2016.2},
  annote =	{Keywords: functional programming, geometry of interaction, categorical semantics, coalgebra}
}
  • Refine by Author
  • 2 Muroya, Koko
  • 1 Ghica, Dan R.
  • 1 Hasuo, Ichiro
  • 1 Sanada, Takahiro
  • 1 Urabe, Natsuki

  • Refine by Classification
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 1 Geometry of Interaction
  • 1 call-by-need reduction
  • 1 categorical semantics
  • 1 coalgebra
  • 1 cost analysis
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2016
  • 1 2017
  • 1 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