Abstract

Haskell is a purely functional, statically typed programming language developed to serve mainly as a tool for programming languages research. Some of its most distinctive features are represented by its strict type checker and automatic type inference engine, which together provide a form of compile-time lightweight formal verification.

This talk will give an example-driven overview of these features: we will go through the basics of constructing Haskell types and then use this knowledge to show how we can define programs that are correct or almost correct by design. Last but not least, we will explore the type system's limitations, i.e., design cases that are impossible or impractical to verify using it.