Extensional Universal Types for Call-by-Value. - Kazuyuki Asada (APLAS, 2008)

Arrows Are Strong Monads. - Kazuyuki Asada (MSFP@ICFP, 2010)

Categorifying Computations into Components via Arrows as Profunctors. - Kazuyuki Asada; Ichiro Hasuo (CMCS@ETAPS, 2010)

Structural recursion for querying ordered graphs. - Soichiro Hidaka; Kazuyuki Asada; Zhenjiang Hu; Hiroyuki Kato; Keisuke Nakano 001 (ICFP, 2013)

A parameterized graph transformation calculus for finite graphs with monadic branches. - Kazuyuki Asada; Soichiro Hidaka; Hiroyuki Kato; Zhenjiang Hu; Keisuke Nakano 001 (PPDP, 2013)

Decision Algorithms for Checking Definability of Order-2 Finitary PCF. - Sadaaki Kawata; Kazuyuki Asada; Naoki Kobayashi 001 (APLAS, 2015)

Refinement Type Checking via Assertion Checking. - Ryosuke Sato 001; Kazuyuki Asada; Naoki Kobayashi 001 (J. Inf. Process., 2015)

On Word and Frontier Languages of Unsafe Higher-Order Grammars. - Kazuyuki Asada; Naoki Kobayashi 001 (ICALP, 2016)

Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. - Ryoma Sin'ya; Kazuyuki Asada; Naoki Kobayashi 001; Takeshi Tsukada (FoSSaCS, 2017)

Pumping Lemma for Higher-order Languages. - Kazuyuki Asada; Naoki Kobayashi 001 (ICALP, 2017)

Generalised species of rigid resource terms. - Takeshi Tsukada; Kazuyuki Asada; C.-H. Luke Ong (LICS, 2017)

A functional reformulation of UnCAL graph-transformations: or, graph transformation as graph reduction. - Kazutaka Matsuda; Kazuyuki Asada (PEPM, 2017)

Verifying relational properties of functional programs by first-order refinement. - Kazuyuki Asada; Ryosuke Sato 001; Naoki Kobayashi 001 (Sci. Comput. Program., 2017)

Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered. - Kazuyuki Asada; Naoki Kobayashi 001 (FSTTCS, 2018)

Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs. - Takeshi Tsukada; Kazuyuki Asada; C.-H. Luke Ong (LICS, 2018)

The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics. - Makoto Hamana; Kazutaka Matsuda; Kazuyuki Asada (Math. Struct. Comput. Sci., 2018)

Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. - Kazuyuki Asada; Naoki Kobayashi 001; Ryoma Sin'ya; Takeshi Tsukada (Log. Methods Comput. Sci., 2019)

Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars. - Kazuyuki Asada; Naoki Kobayashi 001 (FSCD, 2020)

On Average-Case Hardness of Higher-Order Model Checking. - Yoshiki Nakamura 001; Kazuyuki Asada; Naoki Kobayashi 001; Ryoma Sin'ya; Takeshi Tsukada (FSCD, 2020)

A Compositional Approach to Parity Games. - Kazuki Watanabe 003; Clovis Eberhart; Kazuyuki Asada; Ichiro Hasuo (MFPS, 2021)

Streaming ranked-tree-to-string transducers. - Yuta Takahashi; Kazuyuki Asada; Keisuke Nakano 001 (Theor. Comput. Sci., 2021)

Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱. - Takeshi Tsukada; Kazuyuki Asada (LICS, 2022)

On Higher-Order Reachability Games Vs May Reachability. - Kazuyuki Asada; Hiroyuki Katsura; Naoki Kobayashi 001 (RP, 2022)

Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings. - Takeshi Tsukada; Kazuyuki Asada (CoRR, 2022)

Compositional Probabilistic Model Checking with String Diagrams of MDPs. - Kazuki Watanabe 003; Clovis Eberhart; Kazuyuki Asada; Ichiro Hasuo (CAV (3), 2023)

Compositional Solution of Mean Payoff Games by String Diagrams. - Kazuki Watanabe 003; Clovis Eberhart; Kazuyuki Asada; Ichiro Hasuo (Principles of Verification (3), 2024)

Enriched Presheaf Model of Quantum FPC. - Takeshi Tsukada; Kazuyuki Asada (Proc. ACM Program. Lang., 2024)

Characterizations of Partial Well-Behaved Lenses. - Keishi Hashiba; Keisuke Nakano 001; Kazuyuki Asada; Kentaro Kikuchi (PEPM, 2025)