3 papers
cs.LO2026
Solving First-Order Fixed-Point Logics via a Least-to-Greatest Transformation Based on Game Semantics
Satoshi Kura, Hiroshi Unno
Fixed-point logics provide an expressive intermediate framework for reasoning about temporal properties of programs. One of the key approaches to solving their validity checking pr…
cs.LO2026
A Hierarchy of Supermartingales for -Regular Verification
Satoshi Kura, Hiroshi Unno
We propose new supermartingale-based certificates for verifying almost sure satisfaction of -regular properties: (1) generalised Streett supermartingales (GSSMs) and their lexi…
cs.LO2026
A Category-Theoretic Framework for Dependent Effect Systems
Satoshi Kura, Marco Gaboardi, Taro Sekiyama +1
Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfu…