Declarative and Algorithmic Implementation of Refinement Types
F.C. Slothouber (TU Delft - Electrical Engineering, Mathematics and Computer Science)
C.B. Poulsen – Mentor (TU Delft - Programming Languages)
H Van Antwerpen – Mentor (TU Delft - Programming Languages)
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
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.