Typesafe by Definition for Languages with Explicit Deallocation

Typesafe by Definition for Languages with Explicit Deallocation

van den Berg, Rob (TU Delft Electrical Engineering, Mathematics and Computer Science)

Krebbers, R.J. (mentor)

Delft University of Technology

Computer Science and Engineering

CSE3000 Research Project

2018-07-12

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.

Typesafety
Deallocation
Memory management
Definitional interpreter

http://resolver.tudelft.nl/uuid:ebf47756-3895-48cb-bcd8-593c79c560a5

Student theses

bachelor thesis

© 2018 Rob van den Berg