Observatorio de I+D+i UPM

Memorias de investigación
Communications at congresses:
Deriving Interpretations of the Gradually-Typed Lambda Calculus
Year:2014
Research Areas
  • Information technology and adata processing
Information
Abstract
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.
International
Si
Congress
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
960
Place
San Diego, CA, USA
Reviewers
Si
ISBN/ISSN
978-14-5032-619-3
10.1145/2543728.2543742
Start Date
20/01/2014
End Date
21/01/2014
From page
157
To page
168
PEPM '14 Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
Participants
  • Autor: Alvaro Garcia Perez (UPM)
  • Autor: Pablo Nogueira Iglesias (UPM)
  • Autor: Ilya Sergey (Instituto IMDEA Software)
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
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
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)