Sistemas de tipos puros con universos.

Tesis doctoral de Blas Carlos Ruiz Jimenez

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.

 

Datos académicos de la tesis doctoral «Sistemas de tipos puros con universos.«

  • Título de la tesis:  Sistemas de tipos puros con universos.
  • Autor:  Blas Carlos Ruiz Jimenez
  • Universidad:  Málaga
  • Fecha de lectura de la tesis:  01/01/1999

 

Dirección y tribunal

  • Director de la tesis
    • José María Troya Linero
  • Tribunal
    • Presidente del tribunal: Juan jose Moreno navarro
    • Antonio Gavilanes franco (vocal)
    • inmaculada Perez de guzman molina (vocal)
    • buenaventura Clares rodríguez (vocal)

 

Deja un comentario

Tu dirección de correo electrónico no será publicada. Los campos obligatorios están marcados con *

Scroll al inicio