Enhancing expressivity of checked corecursive streams (extended version)
Davide Ancona, Pietro Barbieri, Elena Zucca

TL;DR
This paper introduces an enhanced approach to defining and manipulating streams, allowing for more expressive non-regular streams and ensuring well-defined access through runtime checks, extending previous techniques with new operators.
Contribution
It extends regular corecursion by adding operators and runtime checks, enabling the definition of more complex streams with guaranteed access safety.
Findings
Allows defining non-regular streams
Includes runtime checks for well-defined access
Adds an interleaving combinator with complex recursion
Abstract
We propose a novel approach to stream definition and manipulation. Our solution is based on two key ideas. Regular corecursion, which avoids non termination by detecting cyclic calls, is enhanced, by allowing in equations defining streams other operators besides the stream constructor. In this way, some non-regular streams are definable. Furthermore, execution includes a runtime check to ensure that the stream generated by a function call is well-defined, in the sense that access to an arbitrary index always succeeds. We extend the technique beyond the simple stream operators considered in previous work, notably by adding an interleaving combinator which has a non-trivial recursion scheme.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Software Testing and Debugging Techniques
