Reseña: Certified HLints with Isabelle/HOLCF-Prelude

PorJosé A. Alonso

Se ha publicado un trabajo de verificación formal con Isabelle sobre Haskell titulado Certified HLints with Isabelle/HOLCF-Prelude.

Sus autores son Joachim Breitner, Brian Huffman, Neil Mitchell y Christian Sternagel.

El trabajo se presentará en el HART 2013 ( 1st International Workshop on Haskell And Rewriting Techniques).

Su resumen es

We present the HOLCF-Prelude, a formalization of a large part of Haskell’s standard prelude in Isabelle/HOLCF. Applying this formalization to the hints suggested by HLint allows us to certify them formally.

El códido del HOLCF-Prelude se encuentra aquí.