Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Liquid Haskell: Usable Language-Based Program Verification
Speaker:Niki Vazou
coming from:University of Maryland
Speakers 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.


Event Type:SWS Colloquium
Visibility:SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Monday, 12 February 2018
Duration:90 Minutes
Building:E1 5
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.
Name(s):Annika Meiser
Phone:0681 9303 9105
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:111
Meeting ID:
Tags, Category, Keywords and additional notes
Attachments, File(s):

Annika Meiser/MPI-SWS, 02/07/2018 09:31 AM
Last modified:
Uwe Brahm/MPII/DE, 02/12/2018 07:01 AM
  • Annika Meiser, 02/07/2018 09:34 AM -- Created document.