@thesis{RISC6304,author = {Lucas Payr},
title = {{Refinement Types for Elm}},
language = {english},
abstract = {The aim of this thesis is to add refinement types to Elm. Elm is a pure functional
programming language that uses a Hindley-Miler type system. Refinement types are
subtypes of existing types. These subtypes are defined by a predicate that specifies
which values are part of the subtypes. To extend a Hindley-Miler type system, one
can use so-called liquid types. These are special refinement types that come with an
algorithm for type inference. This algorithm interacts with an SMT solver to solve
subtyping conditions. A type system using liquid types is not complete, meaning not
every valid program can be checked. Instead, liquid types are only defined for a subset
of expressions and only allow specific predicates. In this thesis, we give a formal
definition of the Elm language and its type system. We extend the type system with
liquid types and provide a subset of expressions and a subset of predicates such that
the extended type system is sound. We use the free software system “K Framework”
for rapid prototyping of the formal Elm type system. For rapid prototyping of the
core algorithm of the extended type system we implemented said algorithm in Elm
and checked the subtyping condition in Microsoft’s SMT solver Z3.},
year = {2021},
month = {April},
note = {Also available as RISC report no. 21-10},
translation = {0},
school = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal semantics, formal type systems, programming languages, satisfiability solving},
length = {135},
type = {Master Thesis},
type = {mathesis}
}