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

• Type: Conference
• Year: 1992
• Where: LFP
• Authors: Amr Sabry, Matthias Felleisen
• Keywords: Continuation Passing Style, CPS Terms, CPS Transformation, LFP 1992