Pragmatics of type-directed partial evaluation

Research output: Research - peer-reviewArticle in proceedings

  • Department of Computer Science
Type-directed partial evaluation stems from the residualization of static values in dynamic contexts, given their type and the type of their free variables. Its algorithm coincides with the algorithm for coercing a subtype value into a supertype value, which itself coincides with Berger and Schwichtenberg's normalization algorithm for the simply typed lambda-calculus. Type-directed partial evaluation thus can be used to specialize a compiled, closed program, given its type.
Since Similix, let-insertion is a cornerstone of partial evaluators for call-by-value procedural languages with computational effects (such as divergence). It prevents the duplication of residual computations, and more generally maintains the order of dynamic side effects in the residual program.
This article describes the extension of type-directed partial evaluation to insert residual let expressions. This extension requires the user to annotate arrow types with effect information. It is achieved by delimiting and abstracting control, comparably to continuation-based specialization in direct style. It enables type-directed partial evaluation of programs with effects (e.g., a definitional lambda-interpreter for an imperative language) that are in direct style. The residual programs are in A-normal form. A simple corollary yields CPS (continuation-passing style) terms instead. We illustrate both transformations with two interpreters for Paulson's Tiny language, a classical example in partial evaluation.
Original languageEnglish
Title of host publicationPartial Evaluation : International Seminar Dagstuhl Castle, Germany, February 12–16, 1996 Selected Papers
EditorsOlivier Danvy, Robert Glück, Peter Thiemann
Number of pages22
PublisherSpringer
Publication year1996
Pages73-94
DOIs
StatePublished - 1996
EventInternational Seminar on Partial Evaluation - Dagstuhl , Germany
Duration: 12 Feb 199616 Feb 1996

Conference

ConferenceInternational Seminar on Partial Evaluation
LandGermany
ByDagstuhl
Periode12/02/199616/02/1996
SeriesLecture Notes in Computer Science
Volume1110

See relations at Aarhus University Citationformats

ID: 36019506