Biortogonalidad para corrección de compiladores y adecuación computacional
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.
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | publishedVersion doctoralThesis |
| Lenguaje: | Español |
| Publicado: |
2019
|
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/11086/14324 |
| Aporte de: |
| id |
I10-R141-11086-14324 |
|---|---|
| record_format |
dspace |
| spelling |
I10-R141-11086-143242023-12-13T20:06:06Z Biortogonalidad para corrección de compiladores y adecuación computacional Gadea, Alejandro Emilio Pagano, Miguel María Coherencia Relaciones lógicas Corrección de compiladores Adecuación computacional Mecanización Theory of computation Logic and verification Denotational semantics Categorical semantics Operational semantics Bracketing 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 Gadea, Alejandro Emilio. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. En esta tesis hemos estudiado en profundidad los métodos de biortogonalidad y step-indexing para probar tanto adecuación computacional como corrección de compiladores. Un primer aporte es la prueba de corrección de una semántica denotacional con respecto a una operacional para un lenguaje funcional lazy definido por John Launchbury corriegiendo ciertos ciertas irregularidades en algunas definiciones. Otra contribución es la prueba de adecuación computacional de una semántica operacional con respecto a una denotacional para un lenguaje funcional call-by-value con subtipado. Para este mismo lenguaje probamos la coincidencia entre una semántica denotacional extrínseca y una intrínseca, obteniendo como corolario la coherencia de la semántica intrínseca. Este aporte incluye la mecanización completa en Coq de todos los resultados; siendo, tanto como sabemos, la primera mecanización del teorema de bracketing propuesto por John Reynolds. Finalmente damos una prueba de corrección de un compilador para un lenguaje lazy con recursión generando código para una máquina abstracta, este aporte extiende significativamente un trabajo previo desarrollado por Leonardo Rodríguez. Incluimos también la mecanización completa en Coq. In this work we studied the techniques of biorthogonality and step-indexing for proving computational adequacy and compiler correctness. The first contribution is the proof of correction of a denotational semantics with respect to a operational semantics for a lazy language originally defined by John Launchbury fixing some definition irregularities. Another contribution is the proof of computational adequacy of the operational semantics with respect to a denotational semantics for a call-by-value functional language with subtyping. Also for this same language we prove the coincidence between an extrinsic and intrinsic denotational semantics. This contribution includes the complete mechanization in Coq of all the results; being, as far as we know, the first mechanization of Reynolds’ bracketing theorem. Finally we give a proof of the correction of a compiler for an abstract machine, this contribution significantly extends previous work developed by Leonardo Rodríguez. We also include the complete mechanization in Coq. info:eu-repo/semantics/publishedVersion Gadea, Alejandro Emilio. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2019-12-06T15:36:02Z 2019-12-06T15:36:02Z 2019 doctoralThesis http://hdl.handle.net/11086/14324 spa Atribución-NoComercial-CompartirIgual 4.0 Internacional http://creativecommons.org/licenses/by-nc-sa/4.0/ |
| institution |
Universidad Nacional de Córdoba |
| institution_str |
I-10 |
| repository_str |
R-141 |
| collection |
Repositorio Digital Universitario (UNC) |
| language |
Español |
| topic |
Coherencia Relaciones lógicas Corrección de compiladores Adecuación computacional Mecanización Theory of computation Logic and verification Denotational semantics Categorical semantics Operational semantics Bracketing |
| spellingShingle |
Coherencia Relaciones lógicas Corrección de compiladores Adecuación computacional Mecanización Theory of computation Logic and verification Denotational semantics Categorical semantics Operational semantics Bracketing Gadea, Alejandro Emilio Biortogonalidad para corrección de compiladores y adecuación computacional |
| topic_facet |
Coherencia Relaciones lógicas Corrección de compiladores Adecuación computacional Mecanización Theory of computation Logic and verification Denotational semantics Categorical semantics Operational semantics Bracketing |
| 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 Gadea, Alejandro Emilio |
| format |
publishedVersion doctoralThesis |
| author |
Gadea, Alejandro Emilio |
| author_sort |
Gadea, Alejandro Emilio |
| title |
Biortogonalidad para corrección de compiladores y adecuación computacional |
| title_short |
Biortogonalidad para corrección de compiladores y adecuación computacional |
| title_full |
Biortogonalidad para corrección de compiladores y adecuación computacional |
| title_fullStr |
Biortogonalidad para corrección de compiladores y adecuación computacional |
| title_full_unstemmed |
Biortogonalidad para corrección de compiladores y adecuación computacional |
| title_sort |
biortogonalidad para corrección de compiladores y adecuación computacional |
| publishDate |
2019 |
| url |
http://hdl.handle.net/11086/14324 |
| work_keys_str_mv |
AT gadeaalejandroemilio biortogonalidadparacorrecciondecompiladoresyadecuacioncomputacional |
| _version_ |
1806949514571939840 |