Observatorio de I+D+i UPM

Descripción
Siek and Garcia (2012) have explored the dynamic semantics of the gradually-typed lambda calculus by means of definitional interpreters and abstract machines. The correspondence between the calculus's mathematically described small-step reduction semantics and the implemented big-step definitional interpreters was left as a conjecture. We prove and generalise Siek and Garcia's conjectures using program transformation. We establish the correspondence between the definitional interpreters and the reduction semantics of a closure-converted gradually-typed lambda calculus that unifies and amends various versions of the calculus. We use a layered approach and two-level continuation-passing style so that the correspondence is parametric on the subsidiary coercion calculus. We have implemented the whole derivation for the eager error-detection policy and the downcast blame-tracking strategy. The correspondence can be established for other choices of error-detection policies and blame-tracking strategies, by plugging in the appropriate artefacts for the particular subsidiary coercion calculus.
Internacional	Si
Nombre congreso	ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
Tipo de participación	960
Lugar del congreso	San Diego, CA, USA
Revisores	Si
ISBN o ISSN	978-14-5032-619-3
DOI	10.1145/2543728.2543742
Fecha inicio congreso	20/01/2014
Fecha fin congreso	21/01/2014
Desde la página	157
Hasta la página	168
Título de las actas	PEPM '14 Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

Esta actividad pertenece a memorias de investigación

• Autor: Alvaro Garcia Perez (UPM)
• Autor: Pablo Nogueira Iglesias (UPM)
• Autor: Ilya Sergey (Instituto IMDEA Software)

• Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
• Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software