The Occurrence of Continuation Parameters in CPS Terms.

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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 1995
Accession Number
ADA292952

Entities

People

  • Frank Pfenning
  • Olivier Danvy

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Calculus
  • Case Studies
  • Coding
  • Computer Programming
  • Computer Science
  • Computers
  • Consistency
  • Judgment
  • Language
  • Programming Languages
  • Reasoning
  • Transformers
  • Translations
  • Universities

Readers

  • Computational Linguistics
  • Theoretical Analysis.