Research Assistant Professor
IMDEA Software Institute
Niki dreams of bringing formal verification into everyday programming and she pursues her dream at IMDEA.
Haskell is her favorite programming language because she finds programming with functions the natural way to go and also she never figured out how to prevent null pointer, runtime exceptions.
She started her computer science education in NTUA, Athens, Greece. She earned her Ph.D. at UC San Diego where she and her team developed Liquid Haskell that extends Haskell types with logic with a goal to catch more exceptions before runtime. Since then, she has been pushing to turn Liquid Haskell into a theorem prover, so that all Haskellers can prove random theorems about their programs within Haskell!
After UCSD, she spent some time as a postdoctoral fellow at University of Maryland. Niki's research interests include refinement types, automated program verification, and type systems and her goal is to make theorem proving a useful part of mainstream programming. Liquid Haskell is an SMT-based, refinement type checker for Haskell programs that has been used for various applications ranging from fully automatic light verification of Haskell code, e.g., bound checking, to sophisticated theorem proving, e.g., non-interference.
Talks I've Given
-
Resource Analysis with Refinement Types
Featuring Niki Vazou
Liquid Haskell is an extension of Haskell’s Type system that allows annotating types with refinement predicates. It’s great for ensuring the correctness of your code, but it can also be used to improve the performance of your code.
If you track your resources then Liquid Haskell can be used to...
haskell -
Liquid Haskell: Theorem Proving for All
Featuring Niki Vazou
Formal verification has been gaining the attention and resources of both the academic and the industrial world since it prevents critical software bugs that cost money, energy, time, and even lives. Yet, software development and formal verification are decoupled, requiring verification experts to...
scala scalax haskell functional-programming -
Keynote: Liquid Haskell: Theorem Proving for All
Featuring Niki Vazou
Formal verification has been gaining the attention and resources of both the academic and the industrial world since it prevents critical software bugs that cost money, energy, time, and even lives. Yet, software development and formal verification are decoupled, requiring verification experts to...
keynote haskellx haskell