March 19, 2019
Martin A.T. Handley
Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by encoding logical properties as refinement types. In this interactive talk, I demonstrate how Liquid Haskell can also be used to reason about program efficiency in the same setting, with the system’s existing verification machinery being used to ensure that the results are both meaningful and precise. My experience is that reasoning about efficiency in Liquid Haskell is often just as simple as reasoning about correctness, and even that the two can coincide. I hope to convince you of the same!