Formalización de fundaciones de la matemática y compiladores correctos por construcción

Mostrar todas las versiones(2)

Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019.

Detalles Bibliográficos
Autor principal: Gunther, Emmanuel
Otros Autores: Pagano, Miguel María
Formato: publishedVersion doctoralThesis
Lenguaje:Español
Publicado: 2019
Materias:
Diseño de compiladores
Formalización de matemática
Teoría de conjuntos
Programación con tipos dependientes
Theory of computation
Logic and verification
Software verification
Type Theory
Software and its engineering
Compilers
Forcing
Acceso en línea:http://hdl.handle.net/11086/14372
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-14372
record_format dspace
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Español
topic Diseño de compiladores
Formalización de matemática
Teoría de conjuntos
Programación con tipos dependientes
Theory of computation
Logic and verification
Software verification
Type Theory
Software and its engineering
Compilers
Forcing
spellingShingle Diseño de compiladores
Formalización de matemática
Teoría de conjuntos
Programación con tipos dependientes
Theory of computation
Logic and verification
Software verification
Type Theory
Software and its engineering
Compilers
Forcing
Gunther, Emmanuel
Formalización de fundaciones de la matemática y compiladores correctos por construcción
topic_facet Diseño de compiladores
Formalización de matemática
Teoría de conjuntos
Programación con tipos dependientes
Theory of computation
Logic and verification
Software verification
Type Theory
Software and its engineering
Compilers
Forcing
description Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019.
author2 Pagano, Miguel María
author_facet Pagano, Miguel María
Gunther, Emmanuel
format publishedVersion
doctoralThesis
author Gunther, Emmanuel
author_sort Gunther, Emmanuel
title Formalización de fundaciones de la matemática y compiladores correctos por construcción
title_short Formalización de fundaciones de la matemática y compiladores correctos por construcción
title_full Formalización de fundaciones de la matemática y compiladores correctos por construcción
title_fullStr Formalización de fundaciones de la matemática y compiladores correctos por construcción
title_full_unstemmed Formalización de fundaciones de la matemática y compiladores correctos por construcción
title_sort formalización de fundaciones de la matemática y compiladores correctos por construcción
publishDate 2019
url http://hdl.handle.net/11086/14372
work_keys_str_mv AT guntheremmanuel formalizaciondefundacionesdelamatematicaycompiladorescorrectosporconstruccion
_version_ 1806948218935705600
spelling I10-R141-11086-143722023-12-13T19:39:41Z Formalización de fundaciones de la matemática y compiladores correctos por construcción Gunther, Emmanuel Pagano, Miguel María Diseño de compiladores Formalización de matemática Teoría de conjuntos Programación con tipos dependientes Theory of computation Logic and verification Software verification Type Theory Software and its engineering Compilers Forcing Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2019. info:eu-repo/semantics/publishedVersion Gunther, Emmanuel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Dentro de las teorías fundacionales de la matemática se encuentran la Teoría de Conjuntos y la Teoría de Tipos. La primera es bien conocida en la comunidad matemática; la teoría de tipos además de ser una posible fundación, es una base para lenguajes de programación lo suficientemente expresivos para enunciar teoremas, escribir sus pruebas y que su corrección sea verificada automáticamente. Esta tesis resume tres trabajos independientes pero relacionados entre sí. El primero consiste en el desarrollo de una metodología para definir compiladores correctos por construcción mediante el uso de tipos dependientes. Gracias a la expresividad de estos sistemas de tipos refinamos los lenguajes fuente y destino con su semántica; el tipo de la función de compilación es exactamente la preservación de la semántica. Matemáticamente podemos concebir los lenguajes como álgebras de términos de una signatura y al compilador como el homomorfismo inducido por la interpretación de una signatura en la otra. Esto nos llevó a formalizar en Agda una librería para Álgebra Universal Heterogénea, incluyendo las principales definiciones y resultados básicos, un sistema deductivo para un cálculo ecuacional y las nociones de morfismos entre signaturas y álgebras reducto. El último aporte de la tesis surge del estudio de uno de los problemas más famosos en la teoría de conjuntos: la independencia de la hipótesis del continuo (CH) respecto a la teoría ZFC. Gödel y Cohen demostraron, respectivamente, que no puede refutarse ni probarse CH en ZFC. Cohen desarrolló para ello la técnica de Forcing, que es la única manera conocida para extender modelos de ZFC. Si bien este desarrollo constituye uno de los avances más grandes en teoría de conjuntos, no existe hasta el momento ninguna formalización de Forcing en asistentes de prueba. Como parte de este doctorado hemos comenzado la formalización en el asistente Isabelle/ZF de la técnica de Forcing, llegando a probar que la extensión genérica satisface varios axiomas de ZF. Set Theory and Type Theory are known as Foundations of Mathematics. The first one is well known by mathematicians; Type Theory, besides being a foundation, is the basis for programming languages expressive enough to state theorems, write their proofs and verify their correctness automatically. This thesis summarizes three works. The first one consists of the development of a methodology to define correct-by-construction compilers, using dependent types. Thanks to the expressiveness of these type systems, we refine the syntax of source and target languages by adding information of semantics at type level; then, the type of the compiler function expresses the property of correctness. We can conceive the languages as term algebras of a signature, and the compiler as the homomorphism induced by the interpretation of a signature in other. Hence we formalized in the Agda proof assistant a library of Heterogeneous Universal Algebra, including main definitions and basic results, a deductive system for equational calculus and notions of morphisms between signatures and reduct algebras. The last contribution of this thesis is motivated by the study of one of the most famous problems in set theory: the independence of the continuum hypothesis (CH) with respect to the ZFC theory. Gödel and Cohen showed that CH cannot be refuted or proven. In his work, Cohen developed the technique of forcing, the only known way to extend models of ZFC. Despite the importance of forcing in set theory, there was no mechanization in proof assistants. Our last work consists of the first steps of a complete formalization of forcing in the Isabelle proof assistant. info:eu-repo/semantics/publishedVersion Gunther, Emmanuel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2019-12-10T18:41:49Z 2019-12-10T18:41:49Z 2019 doctoralThesis http://hdl.handle.net/11086/14372 spa Atribución-NoComercial-CompartirIgual 4.0 Internacional http://creativecommons.org/licenses/by-nc-sa/4.0/

Ejemplares similares