Journal article
Reasoning about programs in continuation-passing style.
Abstract
Plotkin's λ-value calculus is sound but incomplete for reasoning about βeegr;-transformations on programs in continuation-passing style (CPS). To find a complete extension, we define a new, compactifying CPS transformation and an “inverse”mapping, un -CPS, both of which are interesting in their own right. Using the new CPS transformation, we can determine the precise language of CPS terms closed under β7eegr;-transformations. Using the un -CPS …
Authors
Sabry A; Felleisen M
Journal
ACM SIGPLAN Lisp Pointers, Vol. V, No. 1, pp. 288–298
Publisher
Association for Computing Machinery (ACM)
Publication Date
January 1992
DOI
10.1145/141478.141563
ISSN
1045-3563