Complete Call-by-Value Calculi of Control Operators, I
Ryu Hasegawa
TL;DR
This paper introduces new call-by-value calculi for control operators that are complete with respect to continuation-passing style semantics, enabling precise characterization of termination properties.
Contribution
It provides the first complete call-by-value calculi for control operators aligned with CPS semantics, along with termination property characterizations.
Findings
Calculi are complete for CPS semantics
Termination properties are characterized using these calculi
Union-intersection type discipline is employed
Abstract
We give new call-by-value calculi of control operators that are complete for the continuation-passing style semantics. Various anticipated computational properties are induced from the completeness. In the first part of a series of papers, we give the characterization of termination properties using the continuation-passing style semantics as well as the union-intersection type discipline.
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
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification