Formalizing, Mechanizing, and Verifying Class-based Refinement Types
@inproceedings{ECOOP:SWC24,
author = {Sun, Ke and Wang, Di and Chen, Sheng and Wang, Meng and Hao, Dan},
booktitle = {European Conf.\ on Object-Oriented Prog.},
doi = {10.4230/LIPIcs.ECOOP.2024.39},
series = {ECOOP'24},
title = {{Formalizing, Mechanizing, and Verifying Class-based Refinement Types}},
year = {2024}
} Abstract
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.