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

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