Reasoning About Programs in Continuation-Passing Style

9 years 2 months ago
Reasoning About Programs in Continuation-Passing Style
The CPS transformation dates back to the early 1970's, where it arose as a technique to represent the control flow of programs in -calculus based programming languages as -terms in the full (free ) -calculus. Toward the end of that decade and afterward, compiler writers found that terms in continuation passing style represented a good intermediate language between their corresponding direct-style (pre-CPS) terms and machine code. Subsequent study of the transformation's theoretical and pragmatic properties led to various refinements on the core algorithm, as well as several "inverse" transformations to produce direct-style terms from CPS terms. These developments led to the investigation of the "essence" of the CPS transform: a set of reduction axioms on source terms, A. Terms in A-Normal Form correspond formally to CPS terms, enabling compiler writers to use optimizations and code generators written for CPS terms on source terms without first having to d...
Amr Sabry, Matthias Felleisen
Added 07 Nov 2010
Updated 07 Nov 2010
Type Conference
Year 1992
Where LFP
Authors Amr Sabry, Matthias Felleisen
Comments (0)