We study some of the applications of category theory to functional programming, particularly in the context of the Haskell functional programming language, and the Agda dependently typed functional programming language and ...

We describe a syntactical proof-reconstruction approach to verify derivations generated by Metis prover to theorems in classical propositional logic -- To verify such derivations, we formalize in type theory each inference ...

¿Por qué incluir un lenguaje de programación en un curso de matemática? ¿Por qué un lenguaje de programación funcional? ¿Por qué Haskell? “Hay una razón fundamental para el estudio integrado de matemática y programación: ...

Este documento presenta una construcción de declaración de tipo que proporciona un sinónimo de tipo, un tipo de datos, un tipo abstracto con vistas, un subtipo de un tipo existente o un módulo (colección de declaraciones), ...

We propose a new approach to computer-assisted verification of lazy functional programs where functions can be defined by general recursion. We work in first-order theories of functional programs which are obtained by ...