Font size: Αα Αα Αα hide gadgets
You are here: Theses » MSc » Niki Vazou Anonymously browsing from at 16:07:01, 21-03-2019. login

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 thesis.


Page updates

No recent updates.

Feeds RSS and Atom feeds

all posts RSS
news RSS
announcements RSS
website news RSS
all events RSS
defenses RSS
exams RSS
seminars RSS
graduations RSS
Web standards: XHTML1.0, CSS3.
© 1996 – 2019 MPLA: Graduate program in Logic, Algorithms and Computation.
Contact the webmaster.