Keynote: Liquid Haskell: Theorem Proving for All
Please log in to watch this conference skillscast.
In this talk, Niki is 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, Niki 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 to prove theorems about Haskell functions by all Haskell programmers.
YOU MAY ALSO LIKE:
Thank you to our sponsors and partners
Platinum
Silver
Partners
Keynote: Liquid Haskell: Theorem Proving for All
Niki Vazou
Research Assistant Professor
IMDEA Software Institute