Hola.
El tipo de una función puede ser visto como una implicación. Si la fórmula es lógicamente válida, la prueba (constructiva) es un término lambda que es un habitante del tipo correspondiente.
En la teoría de tipos que estamos viendo/estudiando, cada enunciado lógico se corresponde con un tipo y cada prueba es un objeto del tipo correspondiente. La identificación de proposiciones con tipos y de pruebas con objetos (términos lambda) es esencialmente el Isomorfismo de Curry-Howard.
Saludos, Carlos