Tipos Dependientes

Una característica teórico-tipológica y familia de sistemas en los que los tipos pueden depender de valores (términos), permitiendo que los tipos expresen especificaciones precisas, relacionen datos y pruebas e internalicen proposiciones como tipos.