|
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 |