Type-checkers are used to verify certain attributes of programs are correct. Avoiding bugs in type-checkers is especially important when accepting faulty programs has serious real-world consequences. Correct-by-construction programming aims to prevent such bugs by embedding proofs of a program's correctness within the program itself. However, this approach introduces different challenges, such as added complexity. Whether the benefits of correct-by-construction type-checkers outweigh these challenges for more complex language features remains uncertain. This paper investigates correct-by-construction type-checking for a toy language with polymorphic algebraic data types and pattern matching. We do this by implementing a type-checker in the dependently typed language Agda. We show that this approach guarantees a type-checker that does not accept ill-typed terms. Furthermore, we reflect on the challenges of this approach and argue that this approach should be used when a guarantee of correctness is required.

The Correct-by-Construction (CbC) programming paradigm has gained increasing attention, particularly with the rise of dependently typed languages. The CbC approach is often characterized as rigid, rule-based construction process making it suitable for critical infrastructure like type-checkers, which are prone to bugs as they become more complex. However, the specific advantages and disadvantages of using the CbC approach for developing type-checkers in comparison to traditional programming languages remain unclear. Therefore, we investigate the development of a type-checker for a toy programming language extended with checked exceptions using the dependently typed programming language Agda. The results show that the CbC approach, combined with dependently typed languages, is highly effective for the very precise task of type-checker development. Despite the steep learning curve associated with these languages, this method offers notable benefits in ensuring the correctness and reliability of type-checkers. We conclude that this approach is a viable strategy for similar projects in the future.

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.