Por Niki Vazou (IMDEA).
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., 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 on the establishment of soundness.
Bio: Niki Vazou works on the theory and applications of refinement type based verification. Currently, he is a research assistant professor at IMDEA Software Institute in Madrid, Spain, before which she did her PhD in University of California, San Diego and a postdoc at University of Maryland. In 2014 she received the Microsoft Research Graduate Fellowship and in 2021 an ERC Starting Grant and a Wallenberg Foundation Fellowship.
