Details of the Researcher

PHOTO

Kazuyuki Asada
Section
Research Institute of Electrical Communication
Job title
Assistant Professor
Degree

Research Interests 9

  • ラムダ計算

  • 形式言語理論

  • 圏論

  • プログラム検証

  • 型理論

  • 関数型プログラミング言語

  • 論理

  • プログラム意味論

  • プログラミング言語

Research Areas 1

  • Informatics / Computational science /

Papers 39

  1. Enriched Presheaf Model of Quantum FPC. Peer-reviewed

    Takeshi Tsukada, Kazuyuki Asada

    Proc. ACM Program. Lang.　8　(POPL)　362-392　2024/01

    DOI： 10.1145/3632855 　

  2. Compositional Probabilistic Model Checking with String Diagrams of MDPs. Peer-reviewed

    Kazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    CAV (3)　40-61　2023

    DOI： 10.1007/978-3-031-37709-9_3 　

  3. Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings Peer-reviewed

    Takeshi Tsukada, Kazuyuki Asada

    LICS　60-13　2022

    DOI： 10.1145/3531130.3533373 　

  4. Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs. Peer-reviewed

    Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong

    Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018　889-898　2018

    Publisher: ACM

    DOI： 10.1145/3209108.3209157 　

  5. Generalised species of rigid resource terms Peer-reviewed

    Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong

    Proceedings - Symposium on Logic in Computer Science　1-12　2017/08/08

    Publisher: Institute of Electrical and Electronics Engineers Inc.

    DOI： 10.1109/LICS.2017.8005093 　

    ISSN： 1043-6871

  6. Pumping Lemma for Higher-order Languages. Peer-reviewed

    Kazuyuki Asada, Naoki Kobayashi

    44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland　97:1-97:14　2017

    Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

  7. On Word and Frontier Languages of Unsafe Higher-Order Grammars. Peer-reviewed

    Kazuyuki Asada, Naoki Kobayashi

    43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy　111:1-111:13　2016

    Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

  8. Structural Recursion for Querying Ordered Graphs Peer-reviewed

    Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

    ACM SIGPLAN NOTICES (ICFP '13: 18th ACM SIGPLAN international conference on Functional programming)　48　(9)　305-318　2013/09

    DOI： 10.1145/2500365.2500608 　

    ISSN： 0362-1340

    eISSN： 1558-1160

  9. Full Definability in a Profunctorial Model.

    Takeshi Tsukada, Kazuyuki Asada, Kengo Hirata

    CoRR　abs/2604.26829　2026/04

    DOI： 10.48550/arXiv.2604.26829 　

  10. PisoLang: a User-Friendly Reversible Programming Language with Inductive Types. Peer-reviewed

    Kosuke Onodera, Keisuke Nakano 0001, Kazuyuki Asada, Kentaro Kikuchi

    RC　219-235　2026

    DOI： 10.1007/978-3-032-30839-9_13 　

  11. Stabilized Profunctors and Matrix Representation. Peer-reviewed

    Takeshi Tsukada, Kazuyuki Asada, Kengo Hirata

    FSCD　34-18　2026

    DOI： 10.4230/LIPIcs.FSCD.2026.34 　

  12. Characterizations of Partial Well-Behaved Lenses. Peer-reviewed

    Keishi Hashiba, Keisuke Nakano 0001, Kazuyuki Asada, Kentaro Kikuchi

    PEPM　43-53　2025

    DOI： 10.1145/3704253.3706139 　

  13. Compositional Solution of Mean Payoff Games by String Diagrams. Peer-reviewed

    Kazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    Principles of Verification (3)　423-445　2025

    DOI： 10.1007/978-3-031-75778-5_20 　

  14. Enriched Presheaf Model of Quantum FPC.

    Takeshi Tsukada, Kazuyuki Asada

    CoRR　abs/2311.03117　2023

    DOI： 10.48550/arXiv.2311.03117 　

  15. Compositional Probabilistic Model Checking with String Diagrams of MDPs.

    Kazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    CoRR　abs/2307.08765　2023

    DOI： 10.48550/arXiv.2307.08765 　

  16. Compositional Solution of Mean Payoff Games by String Diagrams.

    Kazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    CoRR　abs/2307.08034　2023

    DOI： 10.48550/arXiv.2307.08034 　

  17. On Higher-Order Reachability Games Vs May Reachability. Peer-reviewed

    Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi

    Reachability Problems　108-124　2022

    DOI： 10.1007/978-3-031-19135-0_8 　

  18. Streaming ranked-tree-to-string transducers Peer-reviewed

    Yuta Takahashi, Kazuyuki Asada, Keisuke Nakano

    Theoretical Computer Science　870　165-187　2021/05

    Publisher: Elsevier BV

    DOI： 10.1016/j.tcs.2020.12.033 　

    ISSN： 0304-3975

  19. A Compositional Approach to Parity Games Peer-reviewed

    Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo

    Proc. 37th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2021)　abs/2112.14058　278-295　2021

    DOI： 10.4204/EPTCS.351.17 　

  20. Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars. Peer-reviewed

    Kazuyuki Asada, Naoki Kobayashi

    5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)　167　22:1-22:22　2020

    Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik

    DOI： 10.4230/LIPIcs.FSCD.2020.22 　

  21. On Average-Case Hardness of Higher-Order Model Checking. Peer-reviewed

    Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada

    5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)　167　21:1-21:23　2020

    Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik

    DOI： 10.4230/LIPIcs.FSCD.2020.21 　

  22. Streaming Ranked-Tree-to-String Transducers International-journal Peer-reviewed

    Yuta Takahashi, Kazuyuki Asada, Keisuke Nakano

    24th International Conference on Implementation and Application of Automata, CIAA 2019　11601　235-247　2019/07

    Publisher: Springer

    DOI： 10.1007/978-3-030-23679-3_19 　

  23. Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. Peer-reviewed

    Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada

    Logical Methods in Computer Science　15　(1)　1-57　2019

    DOI： 10.23638/LMCS-15(1:16)2019 　

  24. The algebra of recursive graph transformation language UnCAL: Complete axiomatisation and iteration categorical semantics Peer-reviewed

    Makoto Hamana, Kazutaka Matsuda, Kazuyuki Asada

    Mathematical Structures in Computer Science　28　(2)　287-337　2018/02/01

    Publisher: Cambridge University Press

    DOI： 10.1017/S096012951600027X 　

    ISSN： 0960-1295

  25. Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered. Peer-reviewed

    Kazuyuki Asada, Naoki Kobayashi

    38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India　14:1-14:15　2018

    Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

  26. Verifying relational properties of functional programs by first-order refinement Peer-reviewed

    Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

    SCIENCE OF COMPUTER PROGRAMMING　137　2-62　2017/04

    DOI： 10.1016/j.scico.2016.02.007 　

    ISSN： 0167-6423

    eISSN： 1872-7964

  27. Pumping Lemma for Higher-order Languages. Peer-reviewed

    Kazuyuki Asada, Naoki Kobayashi

    CoRR　abs/1705.10699　2017

  28. A Functional Reformulation of UnCAL Graph-Transformations Or, Graph Transformation as Graph Reduction Peer-reviewed

    Kazutaka Matsuda, Kazuyuki Asada

    PROCEEDINGS OF THE 2017 ACM SIGPLAN WORKSHOP ON PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM'17)　71-82　2017

    DOI： 10.1145/3018882.3018883 　

  29. Almost Every Simply Typed lambda-Term Has a Long beta-Reduction Sequence Peer-reviewed

    Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada

    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2017)　10203　53-68　2017

    DOI： 10.1007/978-3-662-54458-7_4 　

    ISSN： 0302-9743

    eISSN： 1611-3349

  30. Refinement type checking via assertion checking Peer-reviewed

    Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

    Journal of Information Processing　23　(6)　827-834　2015/11/15

    Publisher: Information Processing Society of Japan

    DOI： 10.2197/ipsjjip.23.827 　

    ISSN： 1882-6652 0387-5806

  31. Verifying relational properties of functional programs by first-order refinement Peer-reviewed

    Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

    PEPM 2015 - Proceedings of the 2015 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, co-located with POPL 2015　61-72　2015/01/13

    Publisher: Association for Computing Machinery, Inc

    DOI： 10.1145/2678015.2682546 　

  32. The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics. Peer-reviewed

    Makoto Hamana, Kazutaka Matsuda, Kazuyuki Asada

    CoRR　abs/1511.08851　2015

  33. Decision Algorithms for Checking Definability of Order-2 Finitary PCF Peer-reviewed

    Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi

    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2015　9458　313-331　2015

    DOI： 10.1007/978-3-319-26529-2_17 　

    ISSN： 0302-9743

  34. A parameterized graph transformation calculus for finite graphs with monadic branches Peer-reviewed

    Kazuyuki Asada, Soichiro Hidaka, Hiroyuki Kato, Zhenjiang Hu, Keisuke Nakano

    Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP 2013　73-84　2013

    Publisher: ACM

    DOI： 10.1145/2505879.2505903 　

  35. Parameterized Graph Transformation Languages with Monads

    Kazuyuki Asada, Soichiro Hidaka, Hiroyuki Kato, Zhenjiang Hu, Keisuke Nakano

    GRACE Technical Report (GRACE-TR-2012-07)　2012/10

  36. Towards Bidirectional Transformations on Ordered Graphs

    Soichiro Hidaka, Kazuyuki Asada, Hiroyuki Kato, Keisuke Nakano, Zhenjiang Hu

    Technical Report, GRACE Center, National Institute of Informatics (GRACE-TR-2011-07)　2011/12

  37. Categorifying computations into components via arrows as profunctors Peer-reviewed

    Kazuyuki Asada, Ichiro Hasuo

    Electronic Notes in Theoretical Computer Science　264　(2)　25-45　2010/08/10

    DOI： 10.1016/j.entcs.2010.07.012 　

    ISSN： 1571-0661

  38. Arrows are Strong Monads Peer-reviewed

    Kazuyuki Asada

    MSFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN WORKSHOP ON MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING　33-41　2010

    DOI： 10.1145/1863597.1863607 　

  39. Extensional Universal Types for Call-by-Value Peer-reviewed

    Kazuyuki Asada

    PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS　5356　122-137　2008

    DOI： 10.1007/978-3-540-89330-1-9 　 10.1007/978-3-540-89330-1_9 　

    ISSN： 0302-9743

Show all ︎Show first 5

Misc. 3

  1. Refinement Type Checking via Assertion Checking

    Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

    8　(3)　2015/09/21

    ISSN： 1882-7802

  2. Structural Recursion on Ordered Graphs

    29　419-440　2012/08/22

    Publisher: [日本ソフトウェア科学会]

    ISSN： 0913-5391

  3. Semantics of multi-rooted graph and graph algebra

    28　1-7　2011/09/27

    Publisher: [日本ソフトウェア科学会]

    ISSN： 0913-5391

Research Projects 3

  1. 量子計算・確率計算と高級プログラミング言語の融合のための基盤理論

    浅田 和之

    Offer Organization: 日本学術振興会

    System: 科学研究費助成事業

    Category: 基盤研究(C)

    Institution: 東北大学

    2024/04/01 - 2029/03/31

  2. Universal models of programming languages and program reasoning

    Asada Kazuyuki

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research

    Category: Grant-in-Aid for Scientific Research (C)

    Institution: Tohoku University

    2018/04/01 - 2021/03/31

    More details Close

    Our work provides useful models of programming languages equipped with complex computational effects in a general framework. Among these, the model of a functional quantum programming language analyzes a new aspect of the quantum computational effect. This semantic evolution opens many technical challenges, provides ideas to solve them, and makes great progress of the research area. We also studied an application of our theoretical techniques to model checking, and obtained a new algorithm with an implementation.

  3. Integrated and Fundamental for Large-Scale and Practical Bidirectional Graph Transformation

    Hu Zhenjiang, EMOTO Kento, MORIHATA Akimasa, MATSUDA Kazutaka, ZHU Zirun

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (A)

    Category: Grant-in-Aid for Scientific Research (A)

    Institution: National Institute of Informatics

    2013/04/01 - 2017/03/31

    More details Close

    In this research, to realize a bidirectional transformation language that can be used to deal with large scale graphs in practice, we provided a new foundation for bidirectional transformation, showing that the essence of bidirectional transformation is "putback" transformation. Based on this foundation, we succeeded in designing and implementing a new bidirectional transformation language BiGUL, which cannot only fully describe the behavior of bidirectional transformation but also guarantee the roundtrip property. Also, we extended our previous bidirectional graph transformation mechanism so that it can deal with various graph structures, and applied to bidirectionalize model transformations in ATL, a language widely used in model driven software development. Finally, we evaluated the usefulness of our approach by developing several useful systems, including the BiYacc system for supporting development of bidirectional transformations between source programs and abstract syntax trees.