Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Wiring the Pi-calculus to Denotational Semantics
Ken Sakayori, Davide Sangiorgi, Simon Castellan +1
We introduce a dialect of the Asynchronous pi-calculus, called AWpi, in which (1) an input name may be owned, at any time, by at most one process; (2) each name has either only the…
cs.LO2025
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori +1
We propose a novel approach to satisfiability checking of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). CHC-based automated verification has gained considerable…