A Complete Finitary Refinement Type System for Scott-Open Properties
For researchers in programming languages and domain theory, it provides a complete logical framework for verifying properties of recursive functions on infinite data, addressing a known limitation of previous type systems.
The paper presents a finitary refinement type system that is sound and complete for Scott-open properties of functions on infinite data like streams, enabling verification of input-output properties.
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 which is (sound and) complete for Scott-open properties defined in a fixpoint-like logic. Working on top of Abramsky's Domain Theory in Logical Form, we build from the well-known fact that the Scott domains interpreting recursive types are spectral spaces. The usual symmetry between Scott-open and compact-saturated sets is reflected in logical polarities: positive formulae allow for least fixpoints and define Scott-open sets, while negative formulae allow for greatest fixpoints and define compact-saturated sets. A realizability implication with the expected (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.