Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order

García-Pérez, Álvaro; Nogueira, Pablo y Moreno Navarro, Juan José (2013). Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. En: "15th International Symposium on Principles and Practice of Declarative Programming", 16-18 Sep 2013, Madrid, España. ISBN 978-1-4503-2154-9. https://doi.org/10.1145/2505879.2505887.

Descripción

Título: Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order
Autor/es:
  • García-Pérez, Álvaro
  • Nogueira, Pablo
  • Moreno Navarro, Juan José
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: 15th International Symposium on Principles and Practice of Declarative Programming
Fechas del Evento: 16-18 Sep 2013
Lugar del Evento: Madrid, España
Título del Libro: PPDP '13: proceedings of the 15th Symposium on Principles and Practice of Declarative Programming
Fecha: 2013
ISBN: 978-1-4503-2154-9
Materias:
Palabras Clave Informales: Foundations - Lambda calculus - Reduction strategies - Operational semantics - Full reduction - Closures - Explicit substitutions - Program transformation - Reduction semantics - Reductionbased normalisation - Aabstract machines - Reduction-free normalisation
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Lenguajes y Sistemas Informáticos e Ingeniería del Software
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 (1MB) | Vista Previa

Resumen

We derive by program transformation Pierre Crégut s full-reducing Krivine machine KN from the structural operational semantics of the normal order reduction strategy in a closure-converted pure lambda calculus. We thus establish the correspondence between the strategy and the machine, and showcase our technique for deriving full-reducing abstract machines. Actually, the machine we obtain is a slightly optimised version that can work with open terms and may be used in implementations of proof assistants.

Más información

ID de Registro: 30153
Identificador DC: http://oa.upm.es/30153/
Identificador OAI: oai:oa.upm.es:30153
Identificador DOI: 10.1145/2505879.2505887
URL Oficial: http://dl.acm.org/citation.cfm?id=2505887
Depositado por: Memoria Investigacion
Depositado el: 26 Jun 2014 13:21
Ultima Modificación: 22 Abr 2016 00:26
  • 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