Sound-By-Construction Type Systems
Submitted for peer review, July 2025.
Abstract
Type systems for programming languages are usually designed by hand, with the aim of satisfying a type soundness property that guarantees well-typed programs can't go wrong. In this article, we show how standard techniques for proving type soundness can be used in reverse to systematically derive type systems that are sound by construction. We introduce and illustrate our methodology with a series of practical examples, including a typed lambda calculus with conditionals and checked exceptions.
Keywords: Program Calculation, Semantic Types, Type Systems, Logical Relations