Publications
>
Proceedings Paper

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

2-level continuation-passing styleClosuresGradual typesLayered semanticsProgram transformation

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

From the perspective of influence or social adoption, and based on metrics associated with mentions and interactions provided by agencies specializing in calculating the so-called "Alternative or Social Metrics," we can highlight as of 2025-05-31:

  • The use of this contribution in bookmarks, code forks, additions to favorite lists for recurrent reading, as well as general views, indicates that someone is using the publication as a basis for their current work. This may be a notable indicator of future more formal and academic citations. This claim is supported by the result of the "Capture" indicator, which yields a total of: 5 (PlumX).

With a more dissemination-oriented intent and targeting more general audiences, we can observe other more global scores such as:

    It is essential to present evidence supporting full alignment with institutional principles and guidelines on Open Science and the Conservation and Dissemination of Intellectual Heritage. A clear example of this is:

    • The work has been submitted to a journal whose editorial policy allows open Open Access publication.

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