mpla.math.uoa.gr
Font size: Αα Αα Αα hide gadgets
You are here: Defenses » April 2015 » Niki Vazou Anonymously browsing from 54.162.181.75 at 03:08:43, 26-09-2017. 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
Committee:

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.

Reporter

Page updates

No recent updates.

Feeds RSS and Atom feeds

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