Title: Refinement Types

Speaker: Niki Vazou (IMDEA Software Institute in Madrid, Spain)
When: Friday, April 8, 16h30
Where: FCUL, room 6.3.27
(Coffee break included)

Abstract: Refinement types are a type-based, static verification technique designed to be practical. They enrich the types of an existing programming language with logical predicates to specify program properties and automatically validate these specifications using SMT solvers. Refinement types are a promising verification technology that in the last decade has spread to mainstream languages (e.g., Haskell, C, Ruby, Scala, and the ML-family) to verify sophisticated properties of real-world applications, e.g., the safety of cryptographic protocols, memory, and resource usage, and web security. But, the weakness of refinement types is that they do not meet the soundness standards set by theorem provers. In this talk, we will see a brief overview of refinement types, the consequences of their practical design, and the presenter’s future goals for the establishment of soundness.

Bio: Niki Vazou works on the theory and applications of refinement type-based verification. Currently, she is a research assistant professor at IMDEA Software Institute in Madrid, Spain, before which she did her Ph.D. at the University of California, San Diego, and a postdoc at the University of Maryland. In 2014 she received the Microsoft Research Graduate Fellowship and in 2021 an ERC Starting Grant and a Wallenberg Foundation Fellowship.