The Occurrence of Continuation Parameters in CPS Terms.
Olivier Danvy, Frank Pfenning · 1995
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-byvalue -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 machineassisted proof discovery. All the programs are available in ( ftp.daimi.aau.dk:pub/danvy/Programs/danvy-pfenning-Elf93.tar.gz ftp.cs.cmu.edu:user/fp/papers/cpsocc95.tar.gz Most of the research reported here was carried out while the first author visited Carnegie Mellon University in the Spring of 1993. Current address: Olivier Danvy, Ny Munkeg...