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