Infinitary Refinement Types for Temporal Properties in Scott Domains
Colin Riba, Alexandre Kejikian
TL;DR
The paper develops an infinitary refinement-type framework for specifying saturated temporal properties of higher-order programs that manipulate infinite data structures like streams and trees, rooted in Domain Theory in Logical Form (DTLF). It reformulates DTLF to operate with a consistency (instead of coprimeness) predicate and leverages Scott-domain semantics to achieve completeness for a broad class of properties, often without requiring Bonsangue–Kok’s infinitary WF rule. By aiming for a finitary presentation that can simulate infinitary behavior via finite unfoldings, it demonstrates soundness and completeness for key examples (e.g., map, filter, and breadth-first traversal) and positions the approach as an intermediary between denotational semantics and finitary refinement-type systems. The work sets the stage for future extensions toward finitary FPC/CBPV-based systems and broader temporal properties on infinite data types.
Abstract
We discuss an infinitary refinement type system for input-output temporal specifications of functions that handle infinite objects like streams or infinite trees. Our system is based on a reformulation of Bonsangue and Kok's infinitary extension of Abramsky's Domain Theory in Logical Form to saturated properties. We show that in an interesting range of cases, our system is complete without the need of an infinitary rule introduced by Bonsangue and Kok to reflect the well-filteredness of Scott domains.