A Truly Concurrent Game Model of the Asynchronous pi -Calculus. - Ken Sakayori; Takeshi Tsukada (FoSSaCS, 2017)

A Categorical Model of an mathbf i/o -typed pi -calculus. - Ken Sakayori; Takeshi Tsukada (ESOP, 2019)

Termination Analysis for the $$ pi $$-Calculus by Reduction to Sequential Program Termination. - Tsubasa Shoshi; Takuma Ishikawa; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001; Takeshi Tsukada (APLAS, 2021)

Output Without Delay: A π-Calculus Compatible with Categorical Semantics. - Ken Sakayori; Takeshi Tsukada (FSCD, 2021)

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. - Takumi Shimoda; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (SAS, 2021)

Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination. - Tsubasa Shoshi; Takuma Ishikawa; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001; Takeshi Tsukada (CoRR, 2021)

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. - Takumi Shimoda; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (Zenodo, 2021)

Extensional and Non-extensional Functions as Processes. - Ken Sakayori; Davide Sangiorgi (LICS, 2023)

Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem. - Hiroyuki Katsura; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (APLAS, 2024)

Ownership Types for Verification of Programs with Pointer Arithmetic. - Izumi Tanaka; Ken Sakayori; Naoki Kobayashi 001 (PEPM, 2024)

Borrowable Fractional Ownership Types for Verification. - Takashi Nakayama; Yusuke Matsushita 002; Ken Sakayori; Ryosuke Sato 001; Naoki Kobayashi 001 (VMCAI (2), 2024)

Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem. - Hiroyuki Katsura; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (Zenodo, 2024)

On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic. - Risa Yamada; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (ESOP (2), 2025)

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types. - Hiroyuki Katsura; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (SAS, 2025)

On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic. - Risa Yamada; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (Zenodo, 2025)