研究者詳細

顔写真

アサダ　カズユキ
浅田　和之
Kazuyuki Asada
所属
電気通信研究所　計算システム基盤研究部門　コンピューティング情報理論研究室
職名
助教
学位

  • 博士 （京都大学）

研究キーワード 9

  • ラムダ計算

  • 形式言語理論

  • 圏論

  • プログラム検証

  • 型理論

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

  • 論理

  • プログラム意味論

  • プログラミング言語

研究分野 1

  • 情報通信 / 計算科学 / 計算と論理

論文 39

  1. Enriched Presheaf Model of Quantum FPC. 査読有り

    Takeshi Tsukada, Kazuyuki Asada

    Proc. ACM Program. Lang.　8　(POPL)　362-392　2024年1月

    DOI： 10.1145/3632855 　

  2. Compositional Probabilistic Model Checking with String Diagrams of MDPs. 査読有り

    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 査読有り

    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. 査読有り

    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年

    出版者・発行元： ACM

    DOI： 10.1145/3209108.3209157 　

  5. Generalised species of rigid resource terms 査読有り

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

    Proceedings - Symposium on Logic in Computer Science　1-12　2017年8月8日

    出版者・発行元： Institute of Electrical and Electronics Engineers Inc.

    DOI： 10.1109/LICS.2017.8005093 　

    ISSN：1043-6871

  6. Pumping Lemma for Higher-order Languages. 査読有り

    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年

    出版者・発行元： Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

  7. On Word and Frontier Languages of Unsafe Higher-Order Grammars. 査読有り

    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年

    出版者・発行元： Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

  8. Structural Recursion for Querying Ordered Graphs 査読有り

    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年9月

    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年4月

    DOI： 10.48550/arXiv.2604.26829 　

  10. PisoLang: a User-Friendly Reversible Programming Language with Inductive Types. 査読有り

    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. 査読有り

    Takeshi Tsukada, Kazuyuki Asada, Kengo Hirata

    FSCD　34-18　2026年

    DOI： 10.4230/LIPIcs.FSCD.2026.34 　

  12. Characterizations of Partial Well-Behaved Lenses. 査読有り

    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. 査読有り

    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. 査読有り

    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 査読有り

    Yuta Takahashi, Kazuyuki Asada, Keisuke Nakano

    Theoretical Computer Science　870　165-187　2021年5月

    出版者・発行元： Elsevier BV

    DOI： 10.1016/j.tcs.2020.12.033 　

    ISSN：0304-3975

  19. A Compositional Approach to Parity Games 査読有り

    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. 査読有り

    Kazuyuki Asada, Naoki Kobayashi

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

    出版者・発行元： Schloss Dagstuhl - Leibniz-Zentrum für Informatik

    DOI： 10.4230/LIPIcs.FSCD.2020.22 　

  21. On Average-Case Hardness of Higher-Order Model Checking. 査読有り

    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年

    出版者・発行元： Schloss Dagstuhl - Leibniz-Zentrum für Informatik

    DOI： 10.4230/LIPIcs.FSCD.2020.21 　

  22. Streaming Ranked-Tree-to-String Transducers 国際誌 査読有り

    Yuta Takahashi, Kazuyuki Asada, Keisuke Nakano

    24th International Conference on Implementation and Application of Automata, CIAA 2019　11601　235-247　2019年7月

    出版者・発行元： Springer

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

  23. Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. 査読有り

    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 査読有り

    Makoto Hamana, Kazutaka Matsuda, Kazuyuki Asada

    Mathematical Structures in Computer Science　28　(2)　287-337　2018年2月1日

    出版者・発行元： Cambridge University Press

    DOI： 10.1017/S096012951600027X 　

    ISSN：0960-1295

  25. Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered. 査読有り

    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年

    出版者・発行元： Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

  26. Verifying relational properties of functional programs by first-order refinement 査読有り

    Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

    SCIENCE OF COMPUTER PROGRAMMING　137　2-62　2017年4月

    DOI： 10.1016/j.scico.2016.02.007 　

    ISSN：0167-6423

    eISSN：1872-7964

  27. Pumping Lemma for Higher-order Languages. 査読有り

    Kazuyuki Asada, Naoki Kobayashi

    CoRR　abs/1705.10699　2017年

  28. A Functional Reformulation of UnCAL Graph-Transformations Or, Graph Transformation as Graph Reduction 査読有り

    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 λ-Term Has a Long β-Reduction Sequence. 査読有り

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

    Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings　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 査読有り

    Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

    Journal of Information Processing　23　(6)　827-834　2015年11月15日

    出版者・発行元： 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 査読有り

    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年1月13日

    出版者・発行元： 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. 査読有り

    Makoto Hamana, Kazutaka Matsuda, Kazuyuki Asada

    CoRR　abs/1511.08851　2015年

  33. Decision Algorithms for Checking Definability of Order-2 Finitary PCF 査読有り

    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 査読有り

    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年

    出版者・発行元： 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 査読有り

    Kazuyuki Asada, Ichiro Hasuo

    Electronic Notes in Theoretical Computer Science　264　(2)　25-45　2010年8月10日

    DOI： 10.1016/j.entcs.2010.07.012 　

    ISSN：1571-0661

  38. Arrows are Strong Monads 査読有り

    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 査読有り

    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

︎全件表示 ︎最初の5件までを表示

MISC 3

  1. Refinement Type Checking via Assertion Checking

    Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

    情報処理学会論文誌プログラミング（PRO）　8　(3)　2015年9月21日

    ISSN： 1882-7802

    詳細を見る 詳細を閉じる

    A refinement type can be used to express a detailed specification of a higher-order functional program. Given a refinement type as a specification of a program, we can verify that the program satisfies the specification by checking that the program has the refinement type. Refinement type checking/inference has been extensively studied and a number of refinement type checkers have been implemented. Most of the existing refinement type checkers, however, need type annotations, which is a heavy burden on users. To overcome this problem, we reduce a refinement type checking problem to an assertion checking problem, which asks whether the assertions in a program never fail; and then we use an existing assertion checker to solve it. This reduction enables us to construct a fully automated refinement type checker by using a state-of-the-art fully automated assertion checker. We also prove the soundness and the completeness of the reduction, and report on implementation and preliminary experiments.\n------------------------------This is a preprint of an article intended for publication Journal ofInformation Processing(JIP). This preprint should not be cited. Thisarticle should be cited as: Journal of Information Processing Vol.23(2015) No.6(online)------------------------------A refinement type can be used to express a detailed specification of a higher-order functional program. Given a refinement type as a specification of a program, we can verify that the program satisfies the specification by checking that the program has the refinement type. Refinement type checking/inference has been extensively studied and a number of refinement type checkers have been implemented. Most of the existing refinement type checkers, however, need type annotations, which is a heavy burden on users. To overcome this problem, we reduce a refinement type checking problem to an assertion checking problem, which asks whether the assertions in a program never fail; and then we use an existing assertion checker to solve it. This reduction enables us to construct a fully automated refinement type checker by using a state-of-the-art fully automated assertion checker. We also prove the soundness and the completeness of the reduction, and report on implementation and preliminary experiments.\n------------------------------This is a preprint of an article intended for publication Journal ofInformation Processing(JIP). This preprint should not be cited. Thisarticle should be cited as: Journal of Information Processing Vol.23(2015) No.6(online)------------------------------

  2. 順序付き分岐グラフのための構造的再帰

    浅田 和之, 日高 宗一郎, 加藤 弘之

    日本ソフトウェア科学会大会論文集　29　419-440　2012年8月22日

    出版者・発行元： [日本ソフトウェア科学会]

    ISSN： 0913-5391

  3. マルチルートグラフ及びグラフ代数の意味論

    浅田 和之

    日本ソフトウェア科学会大会論文集　28　1-7　2011年9月27日

    出版者・発行元： [日本ソフトウェア科学会]

    ISSN： 0913-5391

共同研究・競争的資金等の研究課題 3

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

    浅田 和之

    2024年4月1日 ～ 2029年3月31日

  2. プログラミング言語の普遍的モデルとプログラム推論

    浅田 和之

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research

    研究種目：Grant-in-Aid for Scientific Research (C)

    研究機関：Tohoku University

    2018年4月1日 ～ 2021年3月31日

    詳細を見る 詳細を閉じる

    2019年度では高階プログラム検証に用いられる高階木文法（非決定性のあるラムダ計算）に関して2本の論文を投稿した（採録は2020年度）． 2018年度の論文において，Kruskalの木定理の高階木文法への拡張の部分的結果を与えるために，変数の使用分析を基底型の変数にのみ着目して行う（交差型を用いない）手法を導入していたが，これは3階の型の項までに制限されていた．2019年度に投稿した当論文ではこの技術を一般の階の項に拡張することで，2016年に与えた「n+1階の高階語文法の成す語言語とn階の高階木文法の生成する木の葉からなる語言語は等しい言語クラスを成す」という（交差型を用いた）結果を計算量の面で改良した．これにより，変換における文法の理論的サイズの増大および計算時間がそれまで超指数的だった計算量を，多項式計算量へと改善させた．これにより，一般に，高階木言語の計算量を伴う結果から高階語言語の結果を系として導出することが容易にできるようになった． 別の論文では高階モデル検査の定量的計算量を分析する研究を行った．この研究では交差型を用いて使用分析の精緻な技術を構築し，それを活用して，2018年度に発表した無限の猿の定理の技術を併用して高階モデル検査の定量的計算量の結果を与えた．高階モデル検査は最悪計算量についてはよく研究されているが，より現実的な計算量である平均計算量の研究はまだなされておらず，本研究はその第一歩を踏み出したものである．またこの使用分析の技術はラムダ計算や高階文法の他の問題へも応用が期待できる．

  3. 大規模な実用に耐えうる双方向グラフ変換の統合的基盤技術の構築

    胡 振江, 加藤 弘之, 中野 圭介, 日高 宗一郎, 浅田 和之, 江本 健斗, 森畑 明昌, 松田 一孝

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (A)

    研究種目：Grant-in-Aid for Scientific Research (A)

    研究機関：National Institute of Informatics

    2013年4月1日 ～ 2017年3月31日

    詳細を見る 詳細を閉じる

    本研究は、大規模な実用に耐えうる双方向グラフ変換のための双方向変換言語の実現を目指して、まず、双方向変換の本質がPutback変換(逆反映変換)である理論を示し、それに基づいた双方向変換の振る舞いを完全に記述しRoundtrip性質を保証できるBiGULの実現に成功した。また、多様なグラフ構造に対応可能な有力な双方向変換を開発し、モデル駆動開発で広く用いられているモデル変換言語ATLの双方向化を行った。さらに、実証研究として、ユーザ向けのソースプログラムとシステム実現向けの抽象構文木の間の双方向変換を開発するためのBiYaccシステムなどを開発し、双方向変換の有効性を確認した。