IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2019 > Liquidate your assets: reasoning about resource usage in Liquid Haskell
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Martin A.T. Handley

martes 19 de marzo de 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!