1 citations · 2 across the 2 of their papers we have counts for
5 papers
Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings
Takeshi Tsukada, Kazuyuki Asada
A number of models of linear logic are based on or closely related to linear algebra, in the sense that morphisms are "matrices" over appropriate coefficient sets. Examples include…
Termination Analysis for the -Calculus by Reduction to Sequential Program Termination
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi +3
We propose an automated method for proving termination of -calculus processes, based on a reduction to termination of sequential programs: we translate a -calculus process to…
A Cyclic Proof System for HFLN
Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFLN, which is a higher-order predicate logic with…
RustHorn: CHC-based Verification for Rust Programs (full version)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointe…
A Type-Based HFL Model Checking Algorithm
Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown th…