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. Log in to add tags.
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



//