mpla.math.uoa.gr
Font size: Αα Αα Αα hide gadgets
You are here: Theses » MSc » Niki Vazou

MSc thesis of Niki Vazou

LiquidHaskell : Liquid Types for Haskell

Supervisor: Nikolaos S. Papaspyrou

Even well-typed programs can go wrong, by returning a wrong answer or throwing a run-time error. A popular response is to allow programmers use refinement type systems to express semantic specifica- tions about programs. We study verification in such systems. On the one hand, expressive refinement type systems require run-time checks or explicit proofs to verify specifications. On the other, less ex- pressive type systems allow static and automatic proofs of the specifications. Next, we present abstract refinement types, a means to enhance the expressiveness of a refinement type system without increas- ing its complexity. Then, we present LiquidHaskell that combines liquidTypes with abstraction over refinements to enhance expressiveness of LiquidTypes. LiquidHaskell is a quite expressive verifica- tion tool for Haskell programs that can be used to check termination, totality and general functional correctness. Finally, we evaluate LiquidHaskell in real world Haskell libraries.

Defended: April 3, 2015.

Scientific committee

Download

Download thesis.

Reporter

Web standards: XHTML1.0, CSS3.
© 1996 – 2018 MPLA: Graduate program in Logic, Algorithms and Computation.
Contact the webmaster.