Resumen de Sistemas de tipos puros con universos
Los Sistemas de Tipo Puros con Universos propuestos en esta tesis permiten modelar de forma apropiada las teorías de tipos y los sistemas lógicos más interesantes, y constituyen el núcleo de la mayoría de los Marcos Lógicos utilizados en la demostración automática de teoremas, Este trabajo propone tales teorías como generalización de otras teorías desarrolladas por un amplio número de investigadores.
Proporciona un estudio general, del cual se pueden obtener propiedades clásicas de muchos sistemas. Desarrolla un original mecanismo algebraico, que es aplicado en la demostración de algunas propiedades no triviales, como la propiedad de "condensación" o la propiedad "decidibilidad del problema de la comprobación de tipos".
Tales propiedades son caracterizadas a través de un simple concepto de conservación de la tipificación bajo reducciones entre universos generalizados.
Sugiere que las herramientas algebraicas desarrolladas son susceptibles de ser utilizadas para resolver otros problemas de la teoría de tipos hoy día aún abiertos.
