Κατάλογος Εκδηλώσεων

Abstract

Refinement types decorate the types of a programming language with logical predicates to allow more expressive type specifications. Originally, refinement type based specifications were restricted to SMT decidable theories and allowed automatic “light” verification, for example properties like non-division by zero or in-bound indexing. In this talk, I will present an overview of refinement types and using Liquid Haskell as the prototype refinement type implementation, will discuss the features that make refinement types a practical verification technology. 

About the Speaker

Niki is an Associate Research Professor at IMDEA Software Institute. She received her Ph.D. at UC San Diego, where she co develop Liquid Haskell, a refinement type checker for Haskell programs. Since then, she works on both the theory of refinement typing and their applications to verify real world properties. For this research purpose, in 2022 she received the ERC Starting Grant CRETE.