Please log in to watch this conference skillscast.
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. Niki's 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, a 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, 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:
- Keynote: Liquid Haskell: Theorem Proving for All (SkillsCast recorded in October 2018)
- Functional Concurrency in .NET with C# and F# (in London on 9th - 10th September 2019)
- Fast Track to F# with Tomas Petricek & Phil Trelford (in London on 9th - 10th September 2019)
- Haskell eXchange 2019 (in London on 10th - 11th October 2019)
- Clojure eXchange 2019 (in London on 2nd - 3rd December 2019)
- Hands-on: Fractal art with Fable and WebGL (in London on 20th June 2019)
- Keynote by Dick Wall on Why API Design Matters, and Why Yours Sucks! (and mine sucks too!) (in London on 24th June 2019)
- The Elements of Tagless Final Style (SkillsCast recorded in May 2019)
- Scala 2.13 and Beyond! (SkillsCast recorded in April 2019)