El isomorfismo de Curry-Howard1 relaciona los sistemas de tipos con la lógica proposicional. Los tipos son teoremas, y las instancias de un tipo son demostraciones del teorema que representa.
A los repositorios del doble grado hemos subido unos apuntes que explican el isomorfismo con su código fuente bajo licencia CC BY-SA 3.0: Isomorfismo de Curry Howard
Los apuntes constan de una presentación general, unos apuntes más detallados, con ejemplos en Haskell y una introducción al asistente de demostraciones Coq. Sobre él, se explican los tipos básicos, demostraciones por inducción y demostraciones explícitas, donde puede verse en acción la correspondencia entre tipos y proposiciones.