Deriving Interpretations of the Gradually-Typed Lambda Calculus
Publicated to:Pepm '14: Proceedings Of The Acm Sigplan Workshop On Partial Evaluation And Program Manipulation. 157-168 - 2014-01-01 (), DOI: 10.1145/2543728.2543742
Authors: Garcia-Perez, Alvaro; Nogueira, Pablo; Sergey, Ilya
Affiliations
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.
Keywords
Quality index
Bibliometric impact. Analysis of the contribution and dissemination channel
From a relative perspective, and based on the normalized impact indicator calculated from the Field Citation Ratio (FCR) of the Dimensions source, it yields a value of: 3.37, which indicates that, compared to works in the same discipline and in the same year of publication, it ranks as a work cited above average. (source consulted: Dimensions May 2025)
Specifically, and according to different indexing agencies, this work has accumulated citations as of 2025-05-31, the following number of citations:
- WoS: 2
- Scopus: 4
- OpenCitations: 3
Impact and social visibility
Leadership analysis of institutional authors
There is a significant leadership presence as some of the institution’s authors appear as the first or last signer, detailed as follows: First Author (GARCIA PEREZ, ALVARO) .