Full text
|
PDF
- Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview |
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.
Title: | Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order |
---|---|
Author/s: |
|
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 |
|
PDF
- Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview |
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.
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 |