2026-07-23T03:47:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20888 2024-09-12T05:48:35Z ddc:004 open_access

Formalizing, Mechanizing, and Verifying Class-Based Refinement Types Sun, Ke Wang, Di Chen, Sheng Wang, Meng Hao, Dan Refinement Types Program Verification Object-oriented Programming Refinement types have been extensively used in class-based languages to specify and verify fine-grained logical specifications. Despite the advances in practical aspects such as applicability and usability, two fundamental issues persist. First, the soundness of existing class-based refinement type systems is inadequately explored, casting doubts on their reliability. Second, the expressiveness of existing systems is limited, restricting the depiction of semantic properties related to object-oriented constructs. This work tackles these issues through a systematic framework. We formalize a declarative class-based refinement type calculus (named RFJ), that is expressive and concise. We rigorously develop the soundness meta-theory of this calculus, followed by its mechanization in Coq. Finally, to ensure the calculus’s verifiability, we propose an algorithmic verification approach based on a fragment of first-order logic (named LFJ), and implement this approach as a type checker. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ke Sun and Di Wang and Sheng Chen and Meng Wang and Dan Hao 2024 Is Part Of LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2024.39 urn:nbn:de:0030-drops-208881 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.39 eng https://creativecommons.org/licenses/by/4.0/legalcode