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

García-Pérez, Álvaro and Nogueira, Pablo and Moreno Navarro, Juan José (2013). Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. In: "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.

Description

Title: Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order
Author/s:
  • García-Pérez, Álvaro
  • Nogueira, Pablo
  • Moreno Navarro, Juan José
Item Type: Presentation at Congress or Conference (Article)
Event Title: 15th International Symposium on Principles and Practice of Declarative Programming
Event Dates: 16-18 Sep 2013
Event Location: Madrid, España
Title of Book: PPDP '13: proceedings of the 15th Symposium on Principles and Practice of Declarative Programming
Date: 2013
ISBN: 978-1-4503-2154-9
Subjects:
Freetext Keywords: Foundations - Lambda calculus - Reduction strategies - Operational semantics - Full reduction - Closures - Explicit substitutions - Program transformation - Reduction semantics - Reductionbased normalisation - Aabstract machines - Reduction-free normalisation
Faculty: Facultad de Informática (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview

Abstract

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.

More information

Item ID: 30153
DC Identifier: http://oa.upm.es/30153/
OAI Identifier: oai:oa.upm.es:30153
DOI: 10.1145/2505879.2505887
Official URL: http://dl.acm.org/citation.cfm?id=2505887
Deposited by: Memoria Investigacion
Deposited on: 26 Jun 2014 13:21
Last Modified: 22 Apr 2016 00:26
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM