Proving ml type soundness within coq

Abstract

We verify within the Coq proof assistant that ML typing is sound with respect to the dynamic semantics. We prove this property in the framework of a big step semantics and also in the framework of a reduction semantics. For that purpose, we use a syntax-directed version of the typing rules: we prove mechanically its equivalence with the initial type system provided by Damas and Milner. This work is complementary to the certification of the ML type inference algorithm done previously by the author and Valerie Menissier-Morain.