Well-Typed Languages are Sound

TL;DR

This paper presents a formal approach and a tool to automatically verify the type soundness of programming languages by ensuring they satisfy progress and preservation theorems through a meta type system.

Contribution

It introduces a meta type system and methodology for guaranteeing language soundness from specifications, with an implementation that automates soundness proofs.

Findings

Successfully applied to languages with recursive types and polymorphism

Automates detection of design mistakes affecting soundness

Produces machine-checked proofs of type soundness

Abstract

Type soundness is an important property of modern programming languages. In this paper we explore the idea that "well-typed languages are sound": the idea that the appropriate typing discipline over language specifications guarantees that the language is type sound. We instantiate this idea for a certain class of languages defined using small step operational semantics by ensuring the progress and preservation theorems. Our first contribution is a syntactic discipline for organizing and restricting language specifications so that they automatically satisfy the progress theorem. This discipline is not novel but makes explicit the way expert language designers have been organizing a certain class of languages for long time. We give a formal account of this discipline by representing language specifications as (higher-order) logic programs and by giving a meta type system over that collection of formulas. Our second contribution is a methodology and meta type system for guaranteeing that languages satisfy the preservation theorem. Ultimately, we proved that language specifications that conform to our meta type systems are guaranteed to be type sound. We have implemented these ideas in the TypeSoundnessCertifier, a tool that takes language specifications in the form of logic programs and type checks them according to our meta type systems. For those languages that pass our type checker, our tool automatically produces a proof of type soundness that can be machine-checked by the Abella proof assistant. For those languages that fail our type checker, the tool pinpoints the design mistakes that hinder type soundness. We have applied the TypeSoundnessCertifier to a large number of programming languages, including those with recursive types, polymorphism, letrec, exceptions, lists and other common types and operators.