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

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.