Infinitary Refinement Types for Temporal Properties in Scott Domains

TL;DR

This paper introduces an infinitary refinement type system for specifying temporal properties of functions over infinite data structures like streams, enhancing the expressiveness and completeness of type-based verification in domain theory.

Contribution

It presents a novel infinitary refinement type system based on a reformulation of domain theory, improving completeness without additional infinitary rules.

Findings

The system is complete for a broad class of cases.

It eliminates the need for certain infinitary rules in type verification.

Applicable to functions handling infinite objects like streams and trees.

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.