Lambda-lifting and CPS conversion in an imperative language
Gabriel Kerneis (PPS), Juliusz Chroboczek (PPS)
TL;DR
This paper provides formal proofs of correctness for lambda-lifting and CPS-conversion techniques in an imperative language, supporting the theoretical foundations of continuation-passing style transformations.
Contribution
It offers the complete formal proofs of lambda-lifting and CPS-conversion correctness, complementing the previous article on Continuation-Passing C.
Findings
Formal proofs of correctness for lambda-lifting
Formal proofs of correctness for CPS-conversion
Supports theoretical understanding of CPS transformations
Abstract
This paper is a companion technical report to the article "Continuation-Passing C: from threads to events through continuations". It contains the complete version of the proofs of correctness of lambda-lifting and CPS-conversion presented in the article.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNatural Language Processing Techniques · Logic, programming, and type systems