DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.28

A Complete Finitary Refinement Type System for Scott-Open Properties

Authors: Colin Riba and Adam Donadille

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

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.

Cite as

Colin Riba and Adam Donadille. A Complete Finitary Refinement Type System for Scott-Open Properties. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{riba_et_al:LIPIcs.FSCD.2026.28,
  author =	{Riba, Colin and Donadille, Adam},
  title =	{{A Complete Finitary Refinement Type System for Scott-Open Properties}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.28},
  URN =		{urn:nbn:de:0030-drops-263780},
  doi =		{10.4230/LIPIcs.FSCD.2026.28},
  annote =	{Keywords: Domain Theory, Temporal Logic, Refinement Types}
}

Search Results

Documents authored by Donadille, Adam

A Complete Finitary Refinement Type System for Scott-Open Properties

Abstract

Cite as

Thanks for your feedback!

Could not send message