Typesafe by Definition for Languages with Explicit Deallocation
Rob van den Berg (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Robbert Krebbers – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
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.