Emmanuel Gunther, 2016-06-15: “Formalización de un framework algebraico para la traducción correcta de lenguajes”.

Next Wednesday, Emmanuel Gunther (FaMAF-UNC) will talk about an application of Universal Algebra to the proof of correctness of a compiler.

Título: Formalización de un framework algebraico para la traducción correcta de lenguajes.

Resumen: Traducir correctamente expresiones de dos lenguajes distintos es una tarea interesante y en general complicada. Dados dos lenguajes $L_1$ y  $L_2$ con alguna semántica definida, un traductor correcto lleva una expresión  $e_1 \in L_1$ a una $e_1 \in L_1$ tal que la semántica de $e_1$ se corresponde con la semántica de $e_2$. Esta correspondencia depende de cada caso en particular.

Este problema puede enfocarse algebraicamente, viendo a los lenguajes como álgebras de términos de signaturas multisort. En varios trabajos se explora este camino para construir compiladores correctos ([1]), y en [2] se presenta un framework general para traducir correctamente lenguajes.

En esta charlita mostraremos una formalización de un framework similar al propuesto en [2], en Agda ([3]). Para ello implementamos las nociones de Signatura, Álgebra, Homomorfismo, Inicialidad y Álgebra de términos, junto con una manera de traducir álgebras de una signatura a otra, obteniendo la prueba de corrección por inicialidad del álgebra de términos.

[1] https://fldit-www.cs.uni-dortmund.de/~peter/MorrisCompiler.pdf
http://www.sciencedirect.com/science/article/pii/0304397581900803
http://www.sciencedirect.com/science/article/pii/S0304397597002703

[2] http://www.phil.uu.nl/ozsl/articles/Janssen03.pdf

[3] http://wiki.portal.chalmers.se/agda/pmwiki.php

Leave a Reply

Your email address will not be published. Required fields are marked *