3 papers
cs.LO2026
A Complete Finitary Refinement Type System for Scott-Open Properties
Colin Riba, Adam Donadille
We are interested in proving input-output properties of functions that handle infinite data such as streams or non-wellfounded trees. We provide a finitary refinement type system w…
cs.LO2025
Infinitary Refinement Types for Temporal Properties in Scott Domains
Colin Riba, Alexandre Kejikian
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 bas…
cs.LO2023
Liveness Properties in Geometric Logic for Domain-Theoretic Streams
Colin Riba, Solal Stern
We devise a version of Linear Temporal Logic (LTL) on a denotational domain of streams. We investigate this logic in terms of domain theory, (point-free) topology and geometric log…