Sistemas de tipos puros con universos
- Ruiz Jiménez, Blas Carlos
- José María Troya Linero Director/a
Universidad de defensa: Universidad de Málaga
Año de defensa: 1999
- Juan José Moreno Navarro Presidente/a
- Ernesto Pimentel Sánchez Secretario/a
- Inmaculada Pérez de Guzmán Molina Vocal
- Antonio Javier Gavilanes Franco Vocal
- Buenaventura Clares Rodríguez Vocal
Tipo: Tesis
Resumen
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.