Sciweavers

TPHOL
2000
IEEE

Proving ML Type Soundness Within Coq

13 years 8 months ago
Proving ML Type Soundness Within Coq
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 Val´erie M´enissier-Morain.
Catherine Dubois
Added 01 Aug 2010
Updated 01 Aug 2010
Type Conference
Year 2000
Where TPHOL
Authors Catherine Dubois
Comments (0)