Sciweavers

Share
ESOP
2016
Springer

Automatically Splitting a Two-Stage Lambda Calculus

4 years 3 months ago
Automatically Splitting a Two-Stage Lambda Calculus
Abstract. Staged programming languages assign a stage to each program expression and evaluate each expression in its assigned stage. A common use of staged languages is to describe programs where inputs arrive at different times or rates. In this paper we present an algorithm for statically splitting these mixed-staged programs into two unstaged, but dependent, programs where the outputs of the first program can be efficiently reused across multiple invocations of the second. While previous algorithms for performing this transformation (also called pass separation and data specialization) were limited to operate on simpler, imperative languages, we define a splitting algorithm for an explicitly-two-stage, typed lambda calculus λ12 with a modality denoting computation at a later stage, and a modality noting purely first-stage code. Most notably, the algorithm splits mixed-stage recursive and higher-order functions. We prove the dynamic correctness of our splitting algorithm with re...
Nicolas Feltman, Carlo Angiuli, Umut A. Acar, Kayv
Added 03 Apr 2016
Updated 03 Apr 2016
Type Journal
Year 2016
Where ESOP
Authors Nicolas Feltman, Carlo Angiuli, Umut A. Acar, Kayvon Fatahalian
Comments (0)
books