Niki Vazou: Practicality and Soundness of Refinement Types

views comments

Abstract:
Refinement types decorate the types of a programming language with logical predicates to allow rnore expressive type specifications. Originally, refinement type based specifications were restricted to SMT decidable theories arnd allowed automatic "light" verification, for example properties like non-division by zero or in-bound indexing. Verification of such light properties though requires "deeper" specifications, for example "is append associative?" or even "does your language preserve typing?" In this talk, I will present an overview of Liquid Haskell's refinement types and discuss if they are practical, general, expressive, and sound.

Bio:
Niki Vazou is an associate research professor at IMDEA Software Institute. She works on verification of functional programming and the foundations and applications of refinement types. Niki did her PhD at uc San Diego where she developed liquid Haskell. She has received the Microsoft Research Fellowship and the ERC Starting Grant.

Speaker home page: https://nikivazou.github.io/

…Read more Less…

Tags

Niki Vazou: Practicality and Soundness of Refinement Types

Related Media