4 papers
Semantic Proof of Confluence of the Categorical Reduction System for Linear Logic
Ryu Hasegawa
We verify a confluence result for the rewriting calculus of the linear category introduced in our previous paper. Together with the termination result proved therein, the generaliz…
A categorical reduction system for linear logic
Ryu Hasegawa
Diagram chasing is not an easy task. The coherence holds in a generalized sense if we have a mechanical method to judge whether given two morphisms are equal to each other. A simpl…
Complete Call-by-Value Calculi of Control Operators, I
Ryu Hasegawa
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…
Complete Call-by-Value Calculi of Control Operators II: Strong Termination
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…