1 Search Results for "Rathke, Julian"


Document
The Lax Braided Structure of Streaming I/O

Authors: Alan Jeffrey and Julian Rathke

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)


Abstract
We investigate and implement a model of typed streaming I/O. Each type determines a language of traces analogous to regular expressions on strings, and programs are modelled by certain monotone functions on these traces. We show that sequential composition forms a lax braided monoid in the category of types and programs. This lax braided structure allows programs to be represented diagrammatically using Joyal and Street's string diagrams in 3D space. Monotone functions over traces cannot be executed efficiently, so we present an equivalent monoidal category of transducers. We demonstrate that transducers can be executed efficiently, theoretically by showing that programs with diagrams embedded in the plane can be executed in O(1) space, and experimentally by an implementation in the Agda dependently typed functional language. Agda supports machine-assisted proof: we have mechanically verified that the transducer implementation and the I/O model form lax braided monoidal categories.

Cite as

Alan Jeffrey and Julian Rathke. The Lax Braided Structure of Streaming I/O. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 292-306, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{jeffrey_et_al:LIPIcs.CSL.2011.292,
  author =	{Jeffrey, Alan and Rathke, Julian},
  title =	{{The Lax Braided Structure of Streaming I/O}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{292--306},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.292},
  URN =		{urn:nbn:de:0030-drops-32386},
  doi =		{10.4230/LIPIcs.CSL.2011.292},
  annote =	{Keywords: semantics, categorical models, streaming I/O, Agda}
}
  • Refine by Author
  • 1 Jeffrey, Alan
  • 1 Rathke, Julian

  • Refine by Classification

  • Refine by Keyword
  • 1 Agda
  • 1 categorical models
  • 1 semantics
  • 1 streaming I/O

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2011

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