mpla.math.uoa.gr
Font size: Αα Αα Αα hide gadgets
You are here: Defenses » Απρίλιος 2015 » Νίκη Βάζου
download defense details: { pdf }

MSc thesis defense presentation

Νίκη Βάζου defends her MSc thesis.

Date: Παρασκευή, 03 Απρ 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

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