Torrens, Paulo, Orchard, Dominic A., Vasconcellos, Cristiano (2024) On the operational theory of the CPS-calculus: Towards a theoretical foundation for IRs. Proceedings of the ACM on Programming Languages, . E-ISSN 2475-1421. (In press) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) (KAR id:106878)
PDF
Updated Version
Language: English Restricted to Repository staff only
This work is licensed under a Creative Commons Attribution 4.0 International License.
|
|
Contact us about this Publication
|
![]() |
Abstract
The continuation-passing style translation often employed by compilers gives rise to a class of intermediate representation languages where functions are not allowed to return anymore. Though the primary use of these intermediate representation languages is to expose details about a program’s control flow, they may be equipped with an equational theory in order to be seen as specialized calculi, which in turn may be related to the original languages by means of a factorization theorem. In this paper, we explore Thielecke’s CPS-calculus, a small theory of continuations inspired by compiler implementations, and study its metatheory. We extend it with a sound reduction semantics that faithfully represents optimization rules used in actual compilers, and prove that it acts as a suitable theoretical foundation for the intermediate representation of Appel’s and Kennedy’s compilers by following the guidelines set out by Plotkin. Finally, we prove that the CPS-calculus is strongly normalizing in the simply typed setting by using a novel proof method for reasoning about reducibility at a distance, from which logical consistency follows. Taken together, these results close a gap in the existing literature, providing a formal theory for reasoning about intermediate representations.
Item Type: | Article |
---|---|
Uncontrolled keywords: | continuations, intermediate representations, strong normalization. |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Dominic Orchard |
Date Deposited: | 13 Aug 2024 16:16 UTC |
Last Modified: | 14 Aug 2024 08:39 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/106878 (The current URI for this page, for reference purposes) |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):