10.4230/LIPICS.CSL.2011.292
Jeffrey, Alan
Alan
Jeffrey
Rathke, Julian
Julian
Rathke
The Lax Braided Structure of Streaming I/O
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
semantics
categorical models
streaming I/O
Agda
Bezem, Marc
Marc
Bezem
2011
2011-08-31
2011-08-31
2011-08-31
en
urn:nbn:de:0030-drops-32386
10.4230/LIPIcs.CSL.2011
978-3-939897-32-3
1868-8969
10.4230/LIPIcs.CSL.2011
LIPIcs, Volume 12, CSL 2011
Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
2013
12
24
292
306
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Bezem, Marc
Marc
Bezem
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
12
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
15 pages
599823 bytes
application/pdf
Creative Commons Attribution-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL, pages 292-306