Typesafe by Definition for Languages with Explicit Deallocation

A definitional interpreter is an interpreter which uses the semantics of its own host language to define those of its object language. Traditionally, a seperate type safety proof is used for such an interpreter. Using a "typesafe-by-construction" approach, where the typesafety is proven by expressing the type system of the object language in the...