Deriving Interpretations of the Gradually-Typed Lambda Calculus
Publicat a:Pepm '14: Proceedings Of The Acm Sigplan Workshop On Partial Evaluation And Program Manipulation. 157-168 - 2014-01-01 (), DOI: 10.1145/2543728.2543742
Autors: Garcia-Perez, Alvaro; Nogueira, Pablo; Sergey, Ilya
Afiliacions
Resum
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.
Paraules clau
Indicis de qualitat
Impacte bibliomètric. Anàlisi de la contribució i canal de difusió
Des d'una perspectiva relativa, i atenent a l'indicador de impacte normalitzat calculat a partir del Field Citation Ratio (FCR) de la font Dimensions, proporciona un valor de: 3.37, el que indica que, comparat amb treballs en la mateixa disciplina i en el mateix any de publicació, el situa com un treball citat per sobre de la mitjana. (font consultada: Dimensions Jun 2025)
Concretament, i atenent a les diferents agències d'indexació, aquest treball ha acumulat, fins a la data 2025-06-01, el següent nombre de cites:
- WoS: 2
- Scopus: 4
- OpenCitations: 3
Impacte i visibilitat social
Anàlisi del lideratge dels autors institucionals
Hi ha un lideratge significatiu, ja que alguns dels autors pertanyents a la institució apareixen com a primer o últim signant, es pot apreciar en el detall: Primer Autor (GARCIA PEREZ, ALVARO) .