Typesafe by Definition for Languages with Explicit Deallocation

Bachelor thesis (2018)

Authors

R.J. van den Berg Electrical Engineering, Mathematics and Computer Science

Contributors

R.J. Krebbers Programming Languages - (mentor)

Faculty

Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science

Typesafety Deallocation Memory management Definitional interpreter

To reference this document use:

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

More Info

expand_more

Published Date

12-07-2018

Language

English

Reuse Rights

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.

Files

Document.pdf

(pdf | 0.277 Mb)