Ryu Hasegawa - Complete Call-by-Value Calculi of Control Operators II: Strong Termination

lmcs:3777 - Logical Methods in Computer Science, March 2, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:18)2021
Complete Call-by-Value Calculi of Control Operators II: Strong TerminationArticle

Authors: Ryu Hasegawa

    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.


    Volume: Volume 17, Issue 1
    Published on: March 2, 2021
    Accepted on: December 8, 2020
    Submitted on: July 10, 2017
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    Consultation statistics

    This page has been seen 861 times.
    This article's PDF has been downloaded 121 times.