6 citations · 14 across the 11 of their papers we have counts for
11 papers
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…
Enriched Presheaf Model of Quantum FPC
Takeshi Tsukada, Kazuyuki Asada
Selinger gave a superoperator model of a first-order quantum programming language and proved that it is fully definable and hence fully abstract. This paper proposes an extension o…
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…
A Compositional Approach to Parity Games
Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada +1
In this paper, we introduce open parity games, which is a compositional approach to parity games. This is achieved by adding open ends to the usual notion of parity games. We intro…
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…
Pumping Lemma for Higher-order Languages
Kazuyuki Asada, Naoki Kobayashi
We study a pumping lemma for the word/tree languages generated by higher-order grammars. Pumping lemmas are known up to order-2 word languages (i.e., for regular/context-free/index…
On Word and Frontier Languages of Unsafe Higher-Order Grammars
Kazuyuki Asada, Naoki Kobayashi
Higher-order grammars are extensions of regular and context-free grammars, where non-terminals may take parameters. They have been extensively studied in 1980's, and restudied rece…
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…