CATÁLOGO DE LA BIBLIOTECA DE LA FaMAF
Normal view MARC view ISBD view

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

By: Pagano, Miguel María, 1979-.
Contributor(s): Coquand, Thierry, 1961- [dir.] | Fridlender, Daniel Edgardo, 1964- [dir.].
Material type: materialTypeLabelBookPublisher: [S.l. : s.n. ], 2012Description: iv, 138 p. : il. ; 30 cm.Subject(s): Mathematical logic | Lógica matemática | Type theory | Normalisation by evaluation | Type-checking algorithm | Martin-Löf type theory | Pure type systems | PTS | Teoría de tipos | Normalización | Algoritmo de chequeo | Teoría de tipos à la Martin-Löf | Sistemas de tipos purosOnline resources: Acceso a Versión Digital Disponible también en líneahttp://www.famaf.unc.edu.ar/publicaciones/documents/serie_d/DComp4.pdfDissertation note: Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2012 Summary: 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.
Tags from this library: No tags from this library for this title.
Item type Current location Call number Copy number Status Notes Date due Barcode Item holds
Tesis de Doctorado Tesis de Doctorado FaMAF
Vitrina
T C PAG 1 Available Ej. de CONSULTA. Disponible también en línea. 21484
Total holds: 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.

Disponible también en línea

http://www.famaf.unc.edu.ar/publicaciones/documents/serie_d/DComp4.pdf

Texto en inglés.

La biblioteca posee 1 ej.

Click on an image to view it in the image viewer

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

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

publicofamaf@gmail.com



//