Construcción Formal de Programas en Teoría de Tipos