2026-07-25T14:47:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20920 2024-09-12T05:53:13Z ddc:004 open_access

Formalizing, Mechanizing, and Verifying Class-Based Refinement Types (Artifact) Sun, Ke Wang, Di Chen, Sheng Wang, Meng Hao, Dan Refinement Types Program Verification Object-oriented Programming This is the artifact description of an ECOOP paper. A new expressive formalization of class-based refinement types is proposed in the paper. We enrich the formalization by analyzing its meta-theory and algorithmic verification. The meta-theory and algorithmic verification have been mechanized and implemented. We discuss details of the mechanization and implementation in this document. 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 DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.10.2.22 urn:nbn:de:0030-drops-209209 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.22 eng https://creativecommons.org/licenses/by/4.0/legalcode