Practicality and Soundness of Refinement Types
by Niki Vazou
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.
More information
Video
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.
More information
Video
Practical information
- General public
- Free
Contact
- Host: Laboratory for Automated Reasoning and Analysis, http://lara.epfl.ch