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 L1 y L2 con alguna semántica definida, un traductor correcto lleva una expresión e1∈L1 a una e1∈L1 tal que la semántica de e1 se corresponde con la semántica de e2. 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
(source)