Continuation marks are a programming language feature which generalize stack inspection. Despite its usefulness, this feature has not been adopted by languages which rely on stack inspection, e.g., for dynamic security checks. One reason for this neglect may be that continuation marks do not yet enjoy a transformation to the plain λ-calculus which would allow higher-order languages to provide continuation marks at little cost. We present a CPS-like transformation from the call-by-value λ-calculus augmented with continuation marks to the pure call-by-value λ-calculus. We discuss how this transformation simplifies the construction of compilers which treat continuation marks correctly. We document an iterative, feedback-based approach using Redex. We accompany the transformation with a meaning-preservation theorem.
| Identifer | oai:union.ndltd.org:BGMYU2/oai:scholarsarchive.byu.edu:etd-4435 |
| Date | 26 November 2012 |
| Creators | Germane, Kimball Richard |
| Publisher | BYU ScholarsArchive |
| Source Sets | Brigham Young University |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | Theses and Dissertations |
| Rights | http://lib.byu.edu/about/copyright/ |
Page generated in 0.0023 seconds