Observatorio de I+D+i UPM

Memorias de investigación
Ponencias en congresos:
Deriving the Full-reducing Krivine Machine from the Small-step Operational Semantics of Normal Order
Año:2013
Áreas de investigación
  • Ciencias de la computación y tecnología informática
Datos
Descripción
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.
Internacional
Si
Nombre congreso
15th Symposium on Principles and Practice of Declarative Programming
Tipo de participación
960
Lugar del congreso
Madrid
Revisores
Si
ISBN o ISSN
978-1-4503-2154-9
DOI
10.1145/2505879.2505887
Fecha inicio congreso
16/09/2013
Fecha fin congreso
18/09/2013
Desde la página
85
Hasta la página
96
Título de las actas
Proceedings of the 15th Symposium on Principles and Practice of declarative Programming
Esta actividad pertenece a memorias de investigación
Participantes
  • Autor: Alvaro Garcia Perez (UPM)
  • Autor: Pablo Nogueira Iglesias (UPM)
  • Autor: Juan Jose Moreno Navarro (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
S2i 2021 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)