Document Open Access Logo

A Complete Finitary Refinement Type System for Scott-Open Properties

Authors Colin Riba , Adam Donadille

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.28.pdf
  • Filesize: 0.82 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Logic and verification
Keywords
  • Domain Theory
  • Temporal Logic
  • Refinement Types

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSCD.2026.28

Author Details

Colin Riba
  • ENS de Lyon, CNRS, Université Claude Bernard Lyon 1, LIP, UMR 5668, 69342, Lyon cedex 07, France
Adam Donadille
  • ENS de Lyon, CNRS, Université Claude Bernard Lyon 1, LIP, UMR 5668, 69342, Lyon cedex 07, France

Funding

This work was partially supported by the French ANR PRCI project ATQUA, ANR-25-CE48-1428-01.

References

  1. S. Abramsky. Domain theory in logical form. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987), pages 47-53. IEEE Computer Society Press, June 1987. Google Scholar
  2. S. Abramsky. Domain Theory in Logical Form. Ann. Pure Appl. Log., 51(1-2):1-77, 1991. URL: https://doi.org/10.1016/0168-0072(91)90065-T.
  3. S. Abramsky and A. Jung. Domain Theory. In S. Abramsky, D.M. Gabbay, and Maibaum T.S.E., editors, Handbook of Logic in Computer Science, chapter 1. Clarendon Press, Oxford, 1995. Google Scholar
  4. R. M. Amadio and P.-L. Curien. Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. Google Scholar
  5. C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  6. U. Berger, R. Matthes, and A. Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In P. Dybjer, J. Espírito Santo, and L. Pinto, editors, Proceedings of TYPES 2018, volume 130 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1:1-1:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.TYPES.2018.1.
  7. M. M. Bonsangue and J. N. Kok. Infinite intersection types. Information and Computation, 186(2):285-318, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00143-3.
  8. J. Bradfield and C. Stirling. Modal Mu-Calculi. In P. Blackburn, J. Van Benthem, and F. Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning, pages 721-756. Elsevier, 2007. URL: https://doi.org/10.1016/S1570-2464(07)80015-2.
  9. M. Bunge and J. Funk. Singular Coverings of Toposes, volume 1890 of Lecture Notes in Mathematics. Springer Berlin Heidelberg, 2006. Google Scholar
  10. T. Coquand and G.-Q. Zhang. Sequents, Frames, and Completeness. In Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, pages 277-291, London, UK, UK, 2000. Springer-Verlag. Google Scholar
  11. M. Dickmann, N. Schwartz, and M. Tressl. Spectral Spaces. New Mathematical Monographs. Cambridge University Press, Cambirdge, 2019. URL: https://doi.org/10.1017/9781316543870.
  12. M. Gehrke and S. van Gool. Topological Duality for Distributive Lattices: Theory and Applications. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2024. Google Scholar
  13. J. Goubault-Larrecq. Non-Hausdorff Topology and Domain Theory: Selected Topics in Point-Set Topology. New Mathematical Monographs. Cambridge University Press, Cambridge, 2013. URL: https://doi.org/10.1017/CBO9781139524438.
  14. I. Hodkinson and M. Reynolds. Temporal Logic. In P. Blackburn, J. Van Benthem, and F. Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning, pages 655-720. Elsevier, 2007. URL: https://doi.org/10.1016/S1570-2464(07)80014-0.
  15. M. Hofmann and W. Chen. Abstract interpretation from Büchi automata. In T. A. Henzinger and D. Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 51:1-51:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603127.
  16. M. Hofmann and J. Ledent. A cartesian-closed category for higher-order model checking. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005120.
  17. M. Huth, A. Jung, and K. Keimel. Linear types and approximation. Mathematical Structures in Computer Science, 10(6):719-745, 2000. URL: http://journals.cambridge.org/action/displayAbstract?aid=71049.
  18. H. Huwig and A. Poigné. A note on inconsistencies caused by fixpoints in a cartesian closed category. Theoretical Computer Science, 73(1):101-112, 1990. URL: https://doi.org/10.1016/0304-3975(90)90165-E.
  19. G. Jaber and C. Riba. Temporal Refinements for Guarded Recursive Types. In N. Yoshida, editor, Proceedins of ESOP'21, volume 12648 of Lecture Notes in Computer Science, pages 548-578. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_20.
  20. P.T. Johnstone. Stone Spaces. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982. Google Scholar
  21. D. O. Kidney and N. Wu. Hyperfunctions: Communicating Continuations. In Proceedings of the 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026). ACM, 2026. URL: https://doi.org/10.1145/3776649.
  22. N. Kobayashi, N. Tabuchi, and H. Unno. Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification. In POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 495-508, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1707801.1706355.
  23. E. Koskinen and T. Terauchi. Local Temporal Reasoning. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS'14, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603138.
  24. J. Lawson. Stably compact spaces. Mathematical Structures in Computer Science, 21(1):125-169, 2011. URL: https://doi.org/10.1017/S0960129510000319.
  25. P. B. Levy. Call-By-Push-Value. Semantics Structures in Computation. Springer, Dordrecht, 2003. URL: https://doi.org/10.1007/978-94-007-0954-6.
  26. P. B. Levy. Call-by-Push-Value. ACM SIGLOG News, 9(2):7-29, May 2022. URL: https://doi.org/10.1145/3537668.3537670.
  27. Y. Nanjo, H. Unno, E. Koskinen, and T. Terauchi. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pages 759-768, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209204.
  28. M. Nygaard and G. Winskel. Full Abstraction for HOPLA. In R.M. Amadio and D. Lugiez, editors, Proceedings of CONCUR 2003, volume 2761 of Lecture Notes in Computer Science, pages 378-392. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45187-7_25.
  29. P. Odifreddi. Classical Recursion Theory, volume 143 of Studies in Logic and the Foundations of Mathematics. Elsevier, second edition, 1999. Google Scholar
  30. B. C. Pierce. Types and Programming Languages. The MIT Press, 1st edition, 2002. Google Scholar
  31. C. Riba and A. Donadille. A Complete Finitary Refinement Type System for Scott-Open Properties. Full version, available on arXiv, January 2026. URL: https://doi.org/10.48550/arXiv.2601.23082.
  32. C. Riba and A. Kejikian. Infinitary Refinement Types for Temporal Properties in Scott Domains. In Proceedings of WoLLIC'25, 2025. Full version available on arXiv (https://arxiv.org/abs/2502.11917). URL: https://doi.org/10.1007/978-3-031-99536-1_11.
  33. C. Riba and S. Stern. Liveness Properties in Geometric Logic for Domain-Theretic Streams. In Proceedings of JFLA'24, 2024. Full version available on arXiv (https://arxiv.org/abs/2310.12763). URL: https://inria.hal.science/hal-04407194.
  34. T. Sekiyama and H. Unno. Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. Proc. ACM Program. Lang., 7(POPL), January 2023. Full version available on arXiv at URL: https://arxiv.org/abs/2207.10386.
  35. C. Skalka, S. Smith, and D. Van Horn. Types and Trace Effects of Higher Order Programs. J. Funct. Program., 18(2):179-249, March 2008. URL: https://doi.org/10.1017/S0956796807006466.
  36. C. Sprenger and M. Dam. On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μ-Calculus. In A. D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pages 425-440. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_27.
  37. T. Streicher. Domain-Theoretic Foundations of Functional Programming. World Scientific, 2006. URL: https://doi.org/10.1142/6284.
  38. H. Unno, Y. Satake, and T. Terauchi. Relatively complete refinement type system for verification of higher-order non-deterministic programs. Proc. ACM Program. Lang., 2(POPL):12:1-12:29, 2018. URL: https://doi.org/10.1145/3158100.
  39. S. Vickers. Topology via Logic. Cambridge University Press, USA, 1989. Google Scholar
  40. S. Vickers. Locales and Toposes as Spaces. In M. Aiello, I. Pratt-Hartman, and J. van Benthem, editors, Handbook of Spatial Logics, chapter 8, pages 429-496. Springer, 2007. URL: https://doi.org/10.1007/978-1-4020-5587-4_8.
  41. G. Winskel. Linearity and nonlinearity in distributed computation. In T. Ehrhard, J.-Y. Girard, and P. Ruet, editors, Linear Logic in Computer Science, London Mathematical Society Lecture Note Series. Cambridge University Press, 2004. Google Scholar
  42. G. Zhang. Logic of Domains. Progress in Theoretical Computer Science. Birkhäuser, Boston, MA, 1991. URL: https://doi.org/10.1007/978-1-4612-0445-9.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact