Punctuated Data Streams

We explore a kind of stream semantics called punctuated
streams. Punctuations in a stream mark the end of substreams, allowing us to view a
non-terminating stream as a mixture of terminating streams. We introduce three kinds of
invariants to specify the proper behavior of query operators in the presence of punctuation.
Pass invariants unblock blocking operators by defining when such an operator can pass
results on. Keep invariants define what must be kept in local state to continue successful
operation. Propagation invariants define when an operator can pass punctuation on. We
then present a strategy for proving that implementations of these invariants are faithful
to their finite table counterparts.

Some definitions could be streamlined, and typos corrected, but otherwise looks interesting.
I also suspect reformulating the definitions in terms of domain theory might have benefited both reader and writer (less implementation-specific details).
On the other hand, category theory might be an overkill for this...

Also, can this be seen as a good application for concurrent constraint programming?
On the first glance punctuations look just like constraints.