Resultados de investigación
Niki Vazou, investigadora del Instituto IMDEA Software, Martin A.T. Handley y Graham Hutton, de la Universidad de Nottingham, Reino Unido, han desarrollado “Liquidate your Assets”, una publicación que presentaron a POPL2020 y que puede consultarse aquí.
Liquid Haskell es una extensión del sistema de tipos de Haskell que permite anotar los tipos con predicados de refinamiento. Es excelente para asegurar la corrección del código, pero también puede utilizarse para mejorar el desempeño del código.
Vazou, Handley y Graham han diseñado e implementado un sistema que permite utilizar Liquid Haskell para razonar formalmente sobre el uso de recursos de los programas puros de Haskell. Además, apoyan el razonamiento sobre las propiedades de corrección y eficiencia de manera combinada y uniforme. “Nuestro sistema toma la forma de una biblioteca y no requiere de modificaciones o extensiones del compilador” comenta Niki Vazou.
Se ha comprobado que el enfoque de una biblioteca para el análisis de costos es correcto con respecto a un modelo subyacente de costo de ejecución utilizando la metateoría de Liquid Haskell.
Al final, han conseguido demostrar la aplicabilidad de la biblioteca en una amplia gama de casos de estudio, que van desde algoritmos de clasificación estándar hasta sofisticadas propiedades de costos relacionales.
