Pragmatics of Type-Directed Partial Evaluation

9 years 18 days ago
Pragmatics of Type-Directed Partial Evaluation
Abstract. Type-directed partial evaluation stems from the residualization of arbitrary static values in dynamic contexts, given their type. Its algorithm coincides with the one for coercing a subtype value into a supertype value, which itself coincides with the one of normalization in the -calculus. Type-directed partial evaluation is thus used to specialize compiled, closed programs, given their type. Since Similix, let-insertion is a cornerstone of partial evaluators for callby-value procedural programs with computational e ects. It prevents the duplication of residual computations, and more generally maintains the order of dynamic side e ects in residual programs. 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 e ect information. It is achieved by delimiting and ing control, comparably to continuation-based specialization in direct style. It enables type-directe...
Olivier Danvy
Added 02 Nov 2010
Updated 02 Nov 2010
Type Conference
Year 1996
Authors Olivier Danvy
Comments (0)