Texto completo
|
PDF (Document Portable Format)
- Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (1MB) | Vista Previa |
Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order
Cita
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: |
|
| 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 |
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 |
