2014/03/13 by Kenneth Knowles, Knowles, Kenneth
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1403.3336
openalex publication_date 2014/03/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 closed under type checking (5) a prototype implementation, Sage, of executable refinement types such that all dynamic errors are communicated back to the compiler and are thenceforth static errors.