IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2019 > Liquidate your assets: reasoning about resource usage in Liquid Haskell

Martin A.T. Handley

Tuesday, March 19, 2019

10:45am Lecture hall 1, level B

Martin A.T. Handley, PhD Student, University of Nottingham, United Kingdom

Liquidate your assets: reasoning about resource usage in Liquid Haskell

Abstract:

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!