Abstract
El Framework Lógico de Edimburgo ha demostrado ser una poderosa herramienta en el
estudio formal de sistemas deductivos, como por ejemplo lenguajes de programación.
Sin embargo su principal implementación, el sistema Twelf, carece de expresividad, obligando
al programador a escribir código repetitivo. Este proyecto presenta una manera
alternativa de utilizar Twelf: a través de un EDSL (Lenguaje Embebido de Dominio Específico)
en Scala que permite representar firmas del Framework Lógico, y apoyándonos
en Twelf como backend para la verificación, abrimos la puerta a diversas posibilidades en
términos de metaprogramación.
El código fuente, así como instrucciones para instalar y configurar, está accesible en
https://github.com/akathorn/elfcala.
---ABSTRACT---The Edinburgh Logical Framework has proven to be to be a powerful tool in the formal
study of deductive systems, such as programming languages. However, its main implementation,
the Twelf system, lacks expressiveness, requiring the programmer to write
repetitive code. This project presents an alternative way of using Twelf: by providing a
Scala EDSL (Embedded Domain Specific Language) that can encode Logical Framework
signatures and relying on Twelf as a backend for the verification, we open the door to
different possibilities in terms of metaprogramming.
The source code, along with instructions to install and configure, is accessible at
https://github.com/akathorn/elfcala
