Correct-by-construction Type Checking for Substructural Type Systems
V. Szabó (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Jesper Cockx – Mentor (TU Delft - Programming Languages)
S. Juhošová – Mentor (TU Delft - Programming Languages)
Thomas Durieux – Graduation committee member (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
As programming languages become ever more sophisticated, there is growing interest in powerful and expressive type systems. Substructural type systems increase expressiveness by allowing the programmer to reason about the number of times and the order in which variables can be used. This can be used to model different kinds of memory allocation and to construct more expressive interfaces. However, implementing complex type systems requires complex type checkers – this complexity increases the chances of bugs in the type checker itself, which could lead to invalid programs being accepted or valid programs being rejected. The consequences of such bugs can range from programmer frustration to critical errors in production systems.
In this thesis, we develop a correct-by-construction type checker for a toy language with a substructural type system. We use Agda’s dependent type system to intrinsically ensure the soundness and completeness of the type checker. We discuss the advantages and disadvantages of the correct-by-construction approach and find that its complexity likely restricts it to specific use cases.