Observatorio de I+D+i UPM

Memorias de investigación
Communications at congresses:
Deriving the Full-reducing Krivine Machine from the Small-step Operational Semantics of Normal Order
Year:2013
Research Areas
  • Information technology and adata processing
Information
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.
International
Si
Congress
15th Symposium on Principles and Practice of Declarative Programming
960
Place
Madrid
Reviewers
Si
ISBN/ISSN
978-1-4503-2154-9
10.1145/2505879.2505887
Start Date
16/09/2013
End Date
18/09/2013
From page
85
To page
96
Proceedings of the 15th Symposium on Principles and Practice of declarative Programming
Participants
  • Autor: Alvaro Garcia Perez (UPM)
  • Autor: Pablo Nogueira Iglesias (UPM)
  • Autor: Juan Jose Moreno Navarro (UPM)
Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
S2i 2019 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)