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 |