A CPS-Like Transformation of Continuation Marks

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 enj...

Full description

Bibliographic Details
Main Author:	Germane, Kimball Richard
Format:	Others
Published:	BYU ScholarsArchive 2012
Subjects:	continuation marks continuation-passing style Redex Computer Sciences
Online Access:	https://scholarsarchive.byu.edu/etd/3436 https://scholarsarchive.byu.edu/cgi/viewcontent.cgi?article=4435&context=etd

id	ndltd-BGMYU2-oai-scholarsarchive.byu.edu-etd-4435
record_format	oai_dc
spelling	ndltd-BGMYU2-oai-scholarsarchive.byu.edu-etd-44352021-08-21T05:01:46Z A CPS-Like Transformation of Continuation Marks Germane, Kimball Richard 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. 2012-11-26T08:00:00Z text application/pdf https://scholarsarchive.byu.edu/etd/3436 https://scholarsarchive.byu.edu/cgi/viewcontent.cgi?article=4435&context=etd http://lib.byu.edu/about/copyright/ Theses and Dissertations BYU ScholarsArchive continuation marks continuation-passing style Redex Computer Sciences
collection	NDLTD
format	Others
sources	NDLTD
topic	continuation marks continuation-passing style Redex Computer Sciences
spellingShingle	continuation marks continuation-passing style Redex Computer Sciences Germane, Kimball Richard A CPS-Like Transformation of Continuation Marks
description	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.
author	Germane, Kimball Richard
author_facet	Germane, Kimball Richard
author_sort	Germane, Kimball Richard
title	A CPS-Like Transformation of Continuation Marks
title_short	A CPS-Like Transformation of Continuation Marks
title_full	A CPS-Like Transformation of Continuation Marks
title_fullStr	A CPS-Like Transformation of Continuation Marks
title_full_unstemmed	A CPS-Like Transformation of Continuation Marks
title_sort	cps-like transformation of continuation marks
publisher	BYU ScholarsArchive
publishDate	2012
url	https://scholarsarchive.byu.edu/etd/3436 https://scholarsarchive.byu.edu/cgi/viewcontent.cgi?article=4435&context=etd
work_keys_str_mv	AT germanekimballrichard acpsliketransformationofcontinuationmarks AT germanekimballrichard cpsliketransformationofcontinuationmarks
_version_	1719460904501772288

A CPS-Like Transformation of Continuation Marks

Similar Items