Embedding logical frameworks in scala

Espino Timón, Daniel (2014). Embedding logical frameworks in scala. Proyecto Fin de Carrera / Trabajo Fin de Grado, E.T.S. de Ingenieros Informáticos (UPM), Madrid, España.

Descripción

Título: Embedding logical frameworks in scala
Autor/es:
  • Espino Timón, Daniel
Director/es:
  • Odersky, Martin
  • Amin, Nada
Tipo de Documento: Proyecto Fin de Carrera/Grado
Grado: Grado en Matemáticas e Informática
Fecha: Junio 2014
Materias:
Escuela: E.T.S. de Ingenieros Informáticos (UPM)
Departamento: Otro
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (325kB) | Vista Previa

Resumen

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

Más información

ID de Registro: 33824
Identificador DC: http://oa.upm.es/33824/
Identificador OAI: oai:oa.upm.es:33824
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 10 Feb 2015 10:11
Ultima Modificación: 28 Oct 2016 09:35
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM