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 type system of the host language is a new approach recently used for imperative languages. In this paper a proof-of-concept is made to show that the technique of "typesafe-byconstruction" can be also applied to interpreters for languages with explicit deallocation. This is done by making such an interpreter for a language called ML-dealloc, which is a basic version of ML extended with explicit allocation and deallocation. The interpreter is written in agda, which type system can be used to express ML-dealloc.CSE3000 Research ProjectComputer Science and Engineerin