Resumen de Cálculo de secuentes para sistemas de tipos puros
LOS SISTEMAS DE TIPOS PUROS FORMAN UN MARCO GENERAL PARA DEFINIR SISTEMAS DE TIPOS QUE USAN INTESIVAMENT TIPOS DEPENDIENTES.
EN ESTA TESIS SE DEFINE UN CÁLCULO SE SECUENTES EQUIVALENTE A LA FORMULACIÓN ESTÁNDAR DE LOS SISTEMAS DE TIPOS PUROS CUYO FRAGMENTO LIBRE DEL CORTE GOZA DE LA PROPIEDAD DE ELIMINACIÓN DEL CORTE EN DOS AMPLÍAS FAMILIAS DE SISTEMAS.
POR MEDIO DEL CÁLCULO ANTERIOR, SE PRUEBA QUE LA PROPIEDAD DE ELIMINACIÓN DEL CORTE RESUELVE EL PROBLEMA DE LA POSPOSICIÓN DE LA BETA-EXPANSIÓN.
FINALMENTE, SE CONSTRUYE UN SEMI-ALGORITMO DE RECONSTRUCCIÓN DE SISTEMAS Y TIPOS NORMALIZADOS TANTO PARA EL CÁLCULO COMPLETO COMO PARA EL FRAGMENTO LIBRE DEL CORTE.
