Reseña: Bind induction: Extracting monadic programs from proofs

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre titulado Bind induction: Extracting monadic programs from proofs.

Sus autores son Hadi Shafei y James Caldwell (de la Univ. de Wyoming).

Su resumen es

Container types can be modeled as foldable monads that support the MonadPlus operations together with a membership operation. In this paper we present a new typeclass we call -Monad that supports a membership operator for instances of the MonadPlus typeclass. The laws for the -Monad typeclass specify how membership behaves with respect to the monad and monad plus operators. Using -Monads we are able write specifications of properties of generic containers. We also present an induction rule for monads we call bind induction. The new proof rule is proved to be sound. The computational content of the new induction rule is a bind operator, using this rule we are able to extract monadic programs from proofs. We present an example that uses the rule to extract a monadic program from a proof of a specification. We have used the Coq theorem prover to formalize the definitions presented here and to prove properties of the formalization. We rely on the Coq Type Class mechanism for our formalization.

El trabajo se ha presentado en el Symposium on Trends in Functional Programming 2014.

El código de las correspondientes teorías en Coq se encuentra en epsilon-Monad.v y decomposition.v.

Reseña: LiquidHaskell: Refinement types in the real world

PorJosé A. Alonso

Se ha publicado un artículo sobre verificación de programas Haskell con LiquidHaskell titulado LiquidHaskell: Refinement types in the real world.

Sus autores son Niki Vazou, Eric L. Seidel y Ranjit Jhala (de la Univ. de California en San Diego).

Su resumen es

Haskell has many delightful features. Perhaps the one most beloved by its users is its type system that allows developers to specify and verify a variety of program properties at compile time. However, many properties, typically those that depend on relationships between program values are impossible, or at the very least, cumbersome to encode within the existing type system. Many such properties can be verified using a combination of Refinement Types and external SMT solvers. We describe the refinement type checker LiquidHaskell, that we have used to specify and verify a variety of properties of over 10,000 lines of Haskell code from various popular libraries, including containers, hscolour, bytestring, text, vector-algorithms and xmonad. First, we present a high-level overview of LiquidHaskell , through a tour of its features. Second, we present a qualitative discussion of the kinds of properties that can be checked – ranging from generic application independent criteria like totality and termination, to application specific concerns like memory safety and data structure correctness invariants. Finally, we present a quantitative evaluation of the approach, with a view towards measuring the efficiency and programmer’s effort required for verification, and discuss the limitations of the approach.

El trabajo se ha presentado en el ACM Haskell Symposium 2014.

I1M2014: El TAD (tipo abstracto de datos) de las tablas en Haskell

PorJosé A. Alonso

En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se ha estudiado cómo trabajar con tablas en Haskell usando el módulo Data.Array y en la segunda parte se ha estudiado el TAD (tipo abstracto de datos) de las tablas y tres implementaciones en Haskell: como funciones, como listas de asociación y como matrices.

Una tabla (array en inglés) es una colección de elementos (valores) a los que se accede mediante sus índices<.

El contenido la segunda parte ha sido el siguiente:

  • la signatura del TAD de las tablas;
  • las propiedades del TAD de las tablas;
  • las implementaciones, en Haskell, de las tablas mediante funciones, listas de asociación y matrices y
  • la comprobación con QuickCheck de sus propiedades.

Read More “I1M2014: El TAD (tipo abstracto de datos) de las tablas en Haskell”