Complete Call-by-Value Calculi of Control Operators II: Strong Termination
Ryu Hasegawa
TL;DR
This paper characterizes the strong termination property of the CCV lambda-mu calculus, linking it to CPS semantics and typeability, and builds on previous work with a union-intersection type system.
Contribution
It provides a characterization of strong termination for the CCV lambda-mu calculus using CPS semantics and typeability, extending prior type system development.
Findings
Strong normalization characterized via CPS semantics.
Typeability corresponds to strong termination.
Completeness of the calculus with respect to CPS semantics.
Abstract
We provide characterization of the strong termination property of the CCV (complete call-by-value) lambda-mu calculus introduced in the first part of this series of the paper. The calculus is complete with respect to the standard continuation-passing style (CPS) semantics. The union-intersection type systems for the calculus is developed in the previous paper. We characterize the strong normalizability of terms of the calculus in terms of the CPS semantics and typeability.
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 · Formal Methods in Verification · Logic, Reasoning, and Knowledge