Sesión Lógica y ComputabilidadRedex $\rightarrow$ Coq
Mallku Soldevila
FAMAF, Universidad Nacional de Córdoba, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
Damos los primeros pasos en el desarrollo de una herramienta para automatizar la traducción de un modelo de semántica de reducciones en Redex, hacia un modelo (idealmente) semánticamente equivalente en Coq. La intención es proporcionar automatización a (algunas partes) de la certificación de propiedades fundamentales de tales modelos. El trabajo se basa originalmente en un modelo de la semántica de Redex [1] desarrollado por Klein et al. Por medio de una generalización simple del problema de encaje de patrones propuesto en [1], obtenemos un algoritmo adecuado para su mecanización en Coq. Para el mismo, demostramos algunas propiedades de corrección, como también su correspondencia con la solución original propuesta por Klein et al. En el proceso, extendemos también el modelo propuesto en [1] con un operador de clausura de Kleene, proporcionando su semántica formal. Resta demostrar las propiedades de corrección deseadas para este modelo final con clausura de Kleene.
Mostraremos también trabajo en progreso sobre el desarrollo de un conjunto de principios generales simples para automatizar la identificación de predicados decidibles sobre semántica de reducciones. De esta manera, esperamos poder ofrecer conceptos primitivos útiles para automatizar la certificación de propiedades de modelos.
Finalmente, discutimos futuras vías de desarrollo que serían habilitadas por este trabajo.
Trabajo en conjunto con: Dr. Beta Ziliani (FAMAF, UNC y Manas.Tech, Argentina).
Referencias
[1] Casey Klein, Jay McCarthy, Steven Jaconette, Robert Bruce Findler (2011) A semantics for context- sensitive reduction semantics. En: APLAS’11.