Observatorio de I+D+i UPM

Memorias de investigación
Ponencias en congresos:
Deriving Interpretations of the Gradually-Typed Lambda Calculus
Año:2014
Áreas de investigación
  • Ciencias de la computación y tecnología informática
Datos
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
Participantes
  • Autor: Alvaro Garcia Perez (UPM)
  • Autor: Pablo Nogueira Iglesias (UPM)
  • Autor: Ilya Sergey (Instituto IMDEA Software)
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
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
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)