Document Open Access Logo

Formalizing, Mechanizing, and Verifying Class-Based Refinement Types (Artifact)

Authors Ke Sun , Di Wang , Sheng Chen , Meng Wang , Dan Hao

PDF
Thumbnail PDF

Artifact Description

DARTS.10.2.22.pdf
  • Filesize: 0.5 MB
  • 3 pages

Document Identifiers

Author Details

Ke Sun
  • Key Lab of HCST (PKU), MOE, School of Computer Science, Peking University, Beijing, China
Di Wang
  • Key Lab of HCST (PKU), MOE, School of Computer Science, Peking University, Beijing, China
Sheng Chen
  • The Center for Advanced Computer Studies, University of Louisiana, Lafayette, LA, USA
Meng Wang
  • University of Bristol, UK
Dan Hao
  • Key Lab of HCST (PKU), MOE, School of Computer Science, Peking University, Beijing, China

Funding

This work is sponsored by National Natural Science Foundation of China Grant No. 62232001, NSF Grant 1750886, and EPSRC Grant EP/T008911/1.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 22:1-22:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/DARTS.10.2.22

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Software and its engineering → Formal software verification
Keywords
  • Refinement Types
  • Program Verification
  • Object-oriented Programming

Metrics

Related Article

  • Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao, "Formalizing, Mechanizing, and Verifying Class-Based Refinement Types", in 38th European Conference on Object-Oriented Programming (ECOOP 2024), LIPIcs, Vol. 313, pp. 39:1-39:30, 2024. https://doi.org/10.4230/LIPIcs.ECOOP.2024.39
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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