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