Should a Function Continue?
Abstract
We show that two lambda-calculus terms can be observationally congruent (i.e., agree in all contexts) but their continuation-passing transforms may not be. We also show that two terms may be congruent in all untyped contexts but fail to be congruent in a language with call/cc operators, and that two terms may have the same meaning in a direct semantics but not in a continuation semantics. Hence, familiar reasoning about terms may be unsound in a setting with continuations, demonstrating the need for a theory of continuations. This document contains corrections to the original thesis submitted in January of 1989.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1989
- Accession Number
- ADA216406
Entities
People
- Jon G. Riecke
Organizations
- Massachusetts Institute of Technology