6 citations · 14 across the 11 of their papers we have counts for
7 papers · 1 filter
Full Definability in a Profunctorial Model
Takeshi Tsukada, Kazuyuki Asada, Kengo Hirata
A semantic model enjoys full definability if every semantic element in the model is a denotation of some proof or program. Full definability indicates that the model captures progr…
Compositional Probabilistic Model Checking with String Diagrams of MDPs
Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada +1
We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language of string diagrams. The algorith…
Compositional Solution of Mean Payoff Games by String Diagrams
Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada +1
Following our recent development of a compositional model checking algorithm for Markov decision processes, we present a compositional framework for solving mean payoff games (MPGs…
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…
On Higher-Order Reachability Games vs May Reachability
Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi
We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with an…
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence
Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya +1
It is well known that the length of a beta-reduction sequence of a simply typed lambda-term of order k can be huge; it is as large as k-fold exponential in the size of the lambda-t…
The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics
Makoto Hamana, Kazutaka Matsuda, Kazuyuki Asada
The aim of this paper is to provide mathematical foundations of a graph transformation language, called UnCAL, using categorical semantics of type theory and fixed points. About tw…