May 7-10, 2017 Asilomar, California
Type soundness is an important property of modern programming
languages. In this talk, we set forth the idea that an appropriate
typing discipline over a language definition can guarantee that the
language is type sound, that is, that well-typed languages are sound.
We have instantiated this idea for a certain class of languages defined using small-step operational semantics. In this talk, I will describe a meta type system that works over the components of a language definition (value declarations, typing rules, reduction rules, evaluation contexts and so on) to ensure that type soundness automatically holds.
We have implemented these ideas in the TypeSoundnessCertifier, a tool for type checking language definitions and certifying their soundness. For those languages that pass our type checker, the tool generates a proof of type soundness that can be machine-checked by a proof assistant. For those languages that fail our type checker, the tool pinpoints the design mistakes that hinder type soundness.
Our research programme strives to demonstrate that ''well-typed languages are sound'' is a scientific perspective that, just like Milner's ''well-typed programs cannot go wrong'', applies across languages and approaches to semantics. Our aim is also to devise type checkers (on language definitions) and automatic certifiers that ensure language properties other than type soundness.