May 7-10, 2017 Asilomar, California
Well-Typed Languages are Sound
Matteo Cimini
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.