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

• Type: Journal
• Year: 2016
• Where: ESOP
• Authors: Nicolas Feltman, Carlo Angiuli, Umut A. Acar, Kayvon Fatahalian
• Keywords: ESOP 2016, Programming Languages