Campus Event Calendar
Event Entry
What and Who
Liquid Haskell: Usable Language-Based Program Verification
Niki Vazou
University of Maryland
SWS Colloquium
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.
Pic: https://nikivazou.github.io/images/me2.jpg
SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 12 February 2018
10:30
90 Minutes
E1 5
029
Saarbrücken
Abstract
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.
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.
Contact
Annika Meiser
0681 9303 9105
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
111
passcode not visible
logged in users only
Annika Meiser, 02/07/2018 09:34 -- Created document.