Formalizing, Mechanizing, and Verifying Class-based Refinement Types
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 that is expressive and concise. We rigorously develop the soundness meta-theory of this calculus, followed by its mechanization in Coq. Finally, we propose an SMT-based verification approach, ensuring the calculus’s verifiability.
Mon 16 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | Types 1Technical Papers at EI 7 Chair(s): Emilio Tuosto Gran Sasso Science Institute, L'Aquila, Italy | ||
13:30 15mTalk | Behavioral up/down casting for statically typed languages Technical Papers Lorenzo Bacchiani University of Bologna, Mario Bravetti Università di Bologna, Marco GIUNTI University of Oxford, João Mota NOVA School of Science and Technology, António Ravara Nova University of Lisbon | ||
13:45 15mTalk | Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency Technical Papers Farzaneh Derakhshan Illinois Institute of Technology, Stephanie Balzer Carnegie Mellon University, Yue Yao Carnegie Mellon University | ||
14:00 15mTalk | Ozone: Fully Out-of-Order Choreographies Technical Papers Dan Plyukhin University of Southern Denmark, Marco Peressotti University of Southern Denmark, Fabrizio Montesi University of Southern Denmark Pre-print | ||
14:15 15mTalk | Information Flow Control in Cyclic Process Networks Technical Papers Bas van den Heuvel Karlsruhe University of Applied Sciences, University of Freiburg, Farzaneh Derakhshan Illinois Institute of Technology, Stephanie Balzer Carnegie Mellon University | ||
14:30 15mTalk | Formalizing, Mechanizing, and Verifying Class-based Refinement Types Technical Papers Ke Sun Peking University, Di Wang Peking University, Sheng Chen UL Lafayette, Meng Wang University of Bristol, Dan Hao Peking University | ||
14:45 15mTalk | Pure methods for roDOT Technical Papers Vlastimil Dort Charles University, Yufeng Li University of Waterloo, Ondřej Lhoták University of Waterloo, Pavel Parizek Charles University | ||