Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation

Olivier Danvy, René Vestergaard

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearch


    We illustrate a simple and effective solution to semantics-based compiling. Our solution is based on ldquotype-directed partial evaluationrdquo, and
    – our compiler generator is expressed in a few lines, and is efficient;
    – its input is a well-typed, purely functional definitional interpreter in the style of denotational semantics;
    – the output of the generated compiler is effectively three-address code, in the fashion and efficiency of the Dragon Book;
    – the generated compiler processes several hundred lines of source code per second.
    The source language considered in this case study is imperative, block-structured, higher-order, call-by-value, allows subtyping, and obeys stack discipline. It is bigger than what is usually reported in the literature on semantics-based compiling and partial evaluation.
    Our compiling technique uses the first Futamura projection, i.e., we compile programs by specializing a definitional interpreter with respect to the program. Specialization is carried out using type-directed partial evaluation, which is a mild version of partial evaluation akin to lambda-calculus normalization.
    Our definitional interpreter follows the format of denotational semantics, with a clear separation between semantic algebras, and valuation functions. It is thus a completely straightforward stack-based interpreter in direct style, which requires no clever staging technique (currying, continuations, binding-time improvements, etc.), and does not rely on any other frame-work (attribute grammars, annotations, etc.) than the typed lambda-calculus. In particular, it uses no other program analysis than traditional type inference. The overall simplicity and effectiveness of the approach has encouraged us to write this paper, to illustrate this genuine solution to denotational semantics-directed compilation, in the spirit of Scott and Strachey. Our conclusion is that lambda-calculus normalization suffices for compiling by specializing an interpreter.
    Original languageEnglish
    Book seriesB R I C S Report Series
    Number of pages28
    Publication statusPublished - 1996


    Dive into the research topics of 'Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation'. Together they form a unique fingerprint.

    Cite this