Imagen de cubierta local
Imagen de cubierta local
Imagen de Google Jackets

Type-Checking and normalisation by evaluation for dependent type systems / Miguel M. Pagano.

Por: Colaborador(es): 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.
Etiquetas de esta biblioteca: No hay etiquetas de esta biblioteca para este título.
Existencias
Tipo de ítem Biblioteca actual Signatura Copia número Estado Notas Fecha de vencimiento Código de barras Reserva de ítems
Tesis de Doctorado Tesis de Doctorado FaMAF Vitrina T C PAG 1 Disponible Ej. de CONSULTA. 21484
Total de reservas: 0

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.

Haga clic en una imagen para verla en el visor de imágenes

Imagen de cubierta local


Nuestras Redes Sociales

facebook Instagram

Horario de la Biblioteca: lunes a viernes de 8:30 a 18:30hs

Av. Medina Allende s/n , Ciudad Universitaria, Córdoba, Argentina

Tel: +54 351 5353701 int. 41127 (Atención al Público) int. 41151 (Dirección)

biblio@famaf.unc.edu.ar (Dirección)

publicofamaf@gmail.com (Atención al público)