Executable Refinement Types
Kenneth Knowles

TL;DR
This dissertation develops executable refinement types that enhance structural types with semi-decidable predicates, providing new theoretical insights and practical tools for undecidable type systems, including a hybrid type checker and a prototype implementation.
Contribution
It introduces a comprehensive framework for executable refinement types, including type soundness, hybrid checking, a decidable reconstruction algorithm, and a prototype implementation.
Findings
Type soundness and logical relation established for executable refinement types
Hybrid type checking outperforms static approximations in some cases
Decidable type reconstruction algorithm implemented in Sage
Abstract
This dissertation introduces executable refinement types, which refine structural types by semi-decidable predicates, and establishes their metatheory and accompanying implementation techniques. These results are useful for undecidable type systems in general. Particular contributions include: (1) Type soundness and a logical relation for extensional equivalence for executable refinement types (though type checking is undecidable); (2) hybrid type checking for executable refinement types, which blends static and dynamic checks in a novel way, in some sense performing better statically than any decidable approximation; (3) a type reconstruction algorithm - reconstruction is decidable even though type checking is not, when suitably redefined to apply to undecidable type systems; (4) a novel use of existential types with dependent types to ensure that the language of logical formulae is…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Parallel Computing and Optimization Techniques
