Infinitary Refinement Types for Temporal Properties in Scott Domains
Logic in Computer Science
2025-05-23 v3
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.
Cite
@article{arxiv.2502.11917,
title = {Infinitary Refinement Types for Temporal Properties in Scott Domains},
author = {Colin Riba and Alexandre Kejikian},
journal= {arXiv preprint arXiv:2502.11917},
year = {2025}
}