Niki Vazou
Developer of Liquid Haskell
Niki is a research assistant professor at IMDEA Software Institute in Madrid.
Before that, she did a PhD at University of California, San Diego and a postdoc at University of Maryland. She developed and maintains Liquid Haskell, a refinement type checker for Haskell programs that aims to make verification as easy as programming in Haskell. Liquid Haskell has been used to verify a variety of properties, ranging from metatheory to enforcement of sophisticated security.
nikivazou.github.io
Refinement Reflection, or how to turn (Liquid) Haskell into a theorem prover
We present Refinement Reflection, a method to extend legacy languages---with highly tuned libraries, compilers, and run-times---into theorem provers.
The key idea is to reflect the code implementing a user-defined function into the function's (output) refinement type.
As a consequence, at uses of the function, the function definition is unfolded into the refinement logic in a precise and predictable manner.
We have implemented our approach in Liquid Haskell thereby retrofitting theorem proving into Haskell.
We show how to use reflection to verify arithmetic properties of common recursive functions as well as program equivalence of computations that use Haskell’s highly tuned parallel runtime environment.
Video ←Back
