Declarative and Algorithmic Implementation of Refinement Types

Bachelor thesis (2019)

Authors

F.C. Slothouber Electrical Engineering, Mathematics and Computer Science

Contributors

C.B. Poulsen Programming Languages - EEMCS (mentor)
H. van Antwerpen Programming Languages - EEMCS (mentor)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2019 Christian Slothouber
More Info
expand_more

Published Date

01-07-2019

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

Type systems and their accompanying checkers provide support for the programmer to write better and safer code, faster, with less effort and with less errors. There are however properties that can not be checked at compile time yet. Refinement types are potentially the solution. They can prove properties of the behaviour of code without actually running and therefore avoid costly bugs in software. This is done by decorating types with predicates that tell something about the value of that type. This paper discusses an implementation of a refinement type system for a functional language.