Focusing on Modular Refinement Typing
Loading...
Authors
Economou, Dimitrios James
Date
2024-09-30
Type
thesis
Language
eng
Keyword
Type refinement
Alternative Title
Abstract
Refinement typing algorithms are hard to design and understand. Liquid Haskell (LH) has powerful features like modular, recursive refinement of inductive data. But Liquid Haskell is relatively hard to understand as it lacks an explicit phase distinction between indices and programs. Index based systems like Dependent ML (DML) tend toward less power but, enjoying an index-program phase distinction, are easier to understand. We apply techniques from logic, type theory, and category theory to design a correct and simple bidirectional typing algorithm for modular recursive index refinements. We use focusing to design logically a call-by-push-value (CBPV) with algebraic datatypes. CBPV is a language known empirically to have good semantic properties even in the presence of computational effects like nontermination and errors. Bidirectional type theories are a reliable way to combine rich type checking and inference. We prove our declarative system is semantically sound for standard mathematical models (domains). We prove our algorithmic system is decidable, sound, complete. Focusing and bidirectional typing combine elegantly with a new concept: value-determined existentials of input types under focus are guaranteed to be solved at the end of focusing stages, clearly outputting constraints decidable by an SMT solver. We believe this work improves our understanding of liquid refinement typing, and we hope it can guide or serve as the foundation for implementations thereof.
Description
Citation
Publisher
License
Queen's University's Thesis/Dissertation Non-Exclusive License for Deposit to QSpace and Library and Archives Canada
ProQuest PhD and Master's Theses International Dissemination Agreement
Intellectual Property Guidelines at Queen's University
Copying and Preserving Your Thesis
This publication is made available by the authority of the copyright owner solely for the purpose of private study and research and may not be copied or reproduced except as permitted by the copyright laws without written authority from the copyright owner.
Attribution-NonCommercial-ShareAlike 4.0 International
ProQuest PhD and Master's Theses International Dissemination Agreement
Intellectual Property Guidelines at Queen's University
Copying and Preserving Your Thesis
This publication is made available by the authority of the copyright owner solely for the purpose of private study and research and may not be copied or reproduced except as permitted by the copyright laws without written authority from the copyright owner.
Attribution-NonCommercial-ShareAlike 4.0 International