Font size: Αα Αα Αα hide gadgets
You are here: Defenses » April 2015 » Niki Vazou Anonymously browsing from at 13:49:26, 21-05-2019. login
download defense details: { pdf }

MSc thesis defense presentation

Niki Vazou defends her MSc thesis.

Date: Friday, 03 Apr 2015
Location: NTUA
Thesis title: LiquidHaskell : Liquid Types for Haskell

Thesis abstract

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.


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.