Este proyecto se desarrollo en el InCo durante los años 1994 a 1997.El objetivo de este proyecto fue el diseño, especificación e implementación de un verificador de pruebas para la teoría Constructiva de Tipos de Martin-Löf con definiciones inductivas de conjuntos y tipos de registros dependientes.
Responsable: Ing. J.J.Cabezas.