Type-Checking and normalisation by evaluation for dependent type systems / Miguel M. Pagano.
Detalles de publicación: [S.l. : s.n. ], 2012.Descripción: iv, 138 p. : il. ; 30 cmTema(s): Nota de disertación: Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2012 Resumen: Esta tesis presenta un nuevo algoritmo de Normalización por Evaluación (NbE) para diferentes teorías de tipos. Utilizamos el algoritmo de normalización para definir un algoritmo de chequeo de tipos y para probar otros meta-teoremas sobre sistemas de tipos predicativos. Asimismo se presenta, una nueva formulación de Sistemas de Tipos Puros (PTS) con sustituciones explícitas e índices de de Bruijn. Hay dos posibles nociones de igualdad entre tipos: igualdad no tipada sobre pre-términos e igualdad tipada; ya se sabía que estas dos presentaciones son equivalentes. Se presenta un nuevo método de prueba para dicha equivalencia para PTS predicativos y se ha formalizado, parcialmente, esta prueba en Agda.Tipo de ítem | Biblioteca actual | Signatura | Copia número | Estado | Notas | Fecha de vencimiento | Código de barras | Reserva de ítems |
---|---|---|---|---|---|---|---|---|
Tesis de Doctorado | FaMAF Vitrina | T C PAG | 1 | Disponible | Ej. de CONSULTA. | 21484 |
Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2012
Bibliografía : p. 129-138.
Esta tesis presenta un nuevo algoritmo de Normalización por Evaluación (NbE) para diferentes teorías de tipos. Utilizamos el algoritmo de normalización para definir un algoritmo de chequeo de tipos y para probar otros meta-teoremas sobre sistemas de tipos predicativos.
Asimismo se presenta, una nueva formulación de Sistemas de Tipos Puros (PTS) con sustituciones explícitas e índices de de Bruijn. Hay dos posibles nociones de igualdad entre tipos: igualdad no tipada sobre pre-términos e igualdad tipada; ya se sabía que estas dos presentaciones son equivalentes. Se presenta un nuevo método de prueba para dicha equivalencia para PTS predicativos y se ha formalizado, parcialmente, esta prueba en Agda.
Texto en inglés.