Publicacions
>
Conferència publicada

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

2-level continuation-passing styleClosuresGradual typesLayered semanticsProgram transformation

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

Des de la dimensió d'influència o adopció social, i prenent com a base les mètriques associades a les mencions i interaccions proporcionades per agències especialitzades en el càlcul de les denominades "Mètriques Alternatives o Socials", podem destacar a data 2025-06-01:

  • L'ús d'aquesta aportació en marcadors, bifurcacions de codi, afegits a llistes de favorits per a una lectura recurrent, així com visualitzacions generals, indica que algú està fent servir la publicació com a base del seu treball actual. Això pot ser un indicador destacat de futures cites més formals i acadèmiques. Aquesta afirmació està avalada pel resultat de l'indicador "Capture", que aporta un total de: 5 (PlumX).

Amb una intenció més de divulgació i orientada a audiències més generals, podem observar altres puntuacions més globals com:

    És fonamental presentar evidències que recolzin l'alineació plena amb els principis i directrius institucionals sobre Ciència Oberta i la Conservació i Difusió del Patrimoni Intel·lectual. Un clar exemple d'això és:

    • El treball s'ha enviat a una revista la política editorial de la qual permet la publicació en obert Open Access.

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