Colloquium Details
Liquid Haskell: Usable Language-Based Program Verification
Speaker: Niki Vazou, University of Maryland
Location: 60 Fifth Avenue 150
Date: March 5, 2018, 2 p.m.
Host: Thomas Wies
Synopsis:
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 prove properties of a template – instead of the actual – implementation ported into verification specific languages. My goal is to bridge formal verification and software development for the programming language Haskell. Haskell is a unique programming language in that it is a general purpose, functional language used for industrial development, but simultaneously it stands at the leading edge of research and teaching welcoming new, experimental, yet useful features.
In this talk I am presenting Liquid Haskell, a refinement type checker in which formal specifications are expressed as a combination of Haskell’s types and expressions and are automatically checked against real Haskell code. This natural integration of specifications in the language, combined with automatic checking, established Liquid Haskell as a usable verifier, enthusiastically accepted by both industrial and academic Haskell users. Recently, I turned Liquid Haskell into a theorem prover, in which arbitrary theorems about Haskell functions would be proved within the language. As a consequence, Liquid Haskell can be used in Haskell courses to teach the principles of mechanized theorem proving.
Turning a general purpose language into a theorem prover opens up new research questions – e.g., can theorems be used for runtime optimizations of existing real-world applications? – that I plan to explore in the future.
Speaker Bio:
Niki Vazou is a Postdoctoral Fellow at the Programming Languages Group at University of Maryland. She completed her Ph.D at UC San Diego, where together with her supervisor Ranjit Jhala, she developed Liquid Haskell, a formal verifier integrated into the Haskell programming language. During her Ph.D she was an intern at MSR Cambridge, MSR Redmond, and Awake Security, where she collaborated with top Haskell researchers and industrial developers on further expanding the applications and foundations of Liquid Haskell. Niki received the MSR Graduate Fellowship and is a member of the HaskellOrg committee.
Notes:
In-person attendance only available to those with active NYU ID cards.