Liquidate your assets: reasoning about resource usage in Liquid Haskell

March 19, 2019

Martin A.T. Handley


Liquidate your assets: reasoning about resource usage in Liquid Haskell

Time:   10:45am
Location:   Lecture hall 1, level B

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!