Tesis doctoral de Francisco Gutiérrez López
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.
Datos académicos de la tesis doctoral «Cálculo de secuentes para sistemas de tipos puros«
- Título de la tesis: Cálculo de secuentes para sistemas de tipos puros
- Autor: Francisco Gutiérrez López
- Universidad: Málaga
- Fecha de lectura de la tesis: 03/12/2003
Dirección y tribunal
- Director de la tesis
- Blas Carlos Ruiz Jimenez
- Tribunal
- Presidente del tribunal: José María Troya linero
- Juan José Moreno navarro (vocal)
- María Alpuente frasnedo (vocal)
- gilles Barthe (vocal)