Accession Number : ADA292952
Title : The Occurrence of Continuation Parameters in CPS Terms.
Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Danvy, Olivier ; Pfenning, Frank
PDF Url : ADA292952
Report Date : FEB 1995
Pagination or Media Count : 24
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)
Descriptors : *COMPUTER LOGIC, *COMPUTER PROGRAMMING, *HIGH LEVEL LANGUAGES, COMPUTER PROGRAM DOCUMENTATION, OPTIMIZATION, PARAMETERS, REASONING, SYNTAX, TRANSFORMATIONS, EXECUTIVE ROUTINES, CONTROL SEQUENCES.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE