The Occurrence of Continuation Parameters in CPS Terms.
- 1 February 1995
- report
- Published by Defense Technical Information Center (DTIC)
Abstract
We prove an occurrence property about formal parameters of continuations in Continuation-Passing Style (CPS) terms that have been automatically produced by CPS transformation of pure, call-by-value lamda-terms. Essentially, parameters of continuations obey a stack-like discipline. This property was introduced, but not formally proven, in an earlier work on the Direct-Style transformation (the inverse of the CPS transformation). The proof has been implemented in Elf, a constraint logic programming language based on the logical framework LF. In fact, it was the implementation that inspired the proof. Thus this note also presents a case study of machine-assisted proof discovery. (AN)Keywords
This publication has 0 references indexed in Scilit: