Sound-by-construction type systems

Patrick Bahr, Zac Garby, and Graham Hutton

In preparation for ICFP ‘26

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 cannot 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.

[pdf] [bib]