Details of the Researcher

PHOTO

Kazutaka Matsuda
Section
Graduate School of Information Sciences
Job title
Associate Professor
Degree

  • 博士（情報理工学）（東京大学）

  • 修士（情報理工学）（東京大学）

Committee Memberships 10

  • 電気情報通信学会　和文マガジン B-Plus 編集委員

    2025/04 - Present

  • 日本ソフトウェア科学会 プログラミング論研究会　運営委員

    2024/04 - Present

  • 日本ソフトウェア科学会　論文誌「コンピュータソフトウェア」編集委員

    2013/04 - Present

  • 日本ソフトウェア科学会 プログラミング論研究会　PPLサマースクール2024 幹事

    2024 - 2024

  • 情報処理学会　論文誌プログラミング編集委員会

    2019/04 - 2023/03

  • 情報処理学会プログラミング研究会　幹事

    2019/04 - 2023/03

  • 情報処理学会東北支部　広報幹事

    2019/04 - 2020/03

  • 情報処理学会プログラミング研究会　運営委員

    2013/04 - 2018/03

  • 情報処理学会　論文誌「プログラミング」編集委員

    2013/04 - 2017/03

  • 情報処理学会　誌「情報処理」編集委員会，FWG委員（ただし2014年4月より同幹事，2015年4月より同主査）

    2011/04 - 2015/03

Show all ︎Show first 5

Professional Memberships 4

  • 電気情報通信学会

  • Association for Computing Machinery

  • 情報処理学会

  • 日本ソフトウェア科学会

Research Interests 4

  • 領域特化言語

  • プログラム変換

  • 関数プログラミング

  • プログラミング言語

Research Areas 2

  • Informatics / Software /

  • Informatics / Information theory /

Awards 1

  1. Best Paper

    2012/01　PEPM 2012　Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals

Papers 40

  1. Reconciling Partial and Local Invertibility Peer-reviewed

    Anders Ågren Thuné, Kazutaka Matsuda, Meng Wang

    Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II　59-89　2024/04/05

    Publisher: Springer Nature Switzerland

    DOI： 10.1007/978-3-031-57267-8_3 　

    ISSN： 0302-9743

    eISSN： 1611-3349

    More details Close

    Abstract Invertible programming languages specify transformations to be run in two directions, such as compression/decompression or encryption/decryption. Two key concepts in invertible programming languages are partial invertibility and local invertibility. Partial invertibility lets invertible code be parameterized by the results of non-invertible code, whereas local invertibility requires all code to be invertible. The former allows for more flexible programming, while the latter has connections to domains such as low-energy computing and quantum computing. We find that existing approaches lack a satisfying treatment of partial invertibility, leaving the connection to local invertibility unclear. In this paper, we identify four core constructs for partially invertible programming, and show how to give them a locally invertible interpretation. We show the expressiveness of the constructs by designing the functional invertible language Kalpis, and show how to give them a locally invertible semantics using the novel arrow combinator language $$\textsc {rrArr}$$—the key idea is viewing partial invertibility as an invertible effect. By formalizing the two systems and giving Kalpis semantics by translation to $$\textsc {rrArr}$$, we reconcile partial and local invertibility, solving an open problem in the field. All formal developments are mechanized in Agda.

  2. Sparcl: A language for partially invertible computation Peer-reviewed

    Kazutaka Matsuda, Meng Wang

    J. Funct. Program.　34　2024

    DOI： 10.1017/s0956796823000126 　

  3. Embedding by Unembedding Peer-reviewed

    Kazutaka Matsuda, Samantha Frohlich, Meng Wang, Nicolas Wu

    Proceedings of the ACM on Programming Languages　7　(ICFP)　1-47　2023/08

    DOI： 10.1145/3607830 　

  4. Synbit: synthesizing bidirectional programs using unidirectional sketches Peer-reviewed

    Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

    Formal Methods Syst. Des.　61　(2)　198-247　2022/12

    DOI： 10.1007/s10703-023-00436-9 　

  5. Synbit: synthesizing bidirectional programs using unidirectional sketches Peer-reviewed

    Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

    Proceedings of the ACM on Programming Languages　5　(OOPSLA)　1-31　2021

    DOI： 10.1145/3485482 　

  6. Modular Inference of Linear Types for Multiplicity-Annotated Arrows Peer-reviewed

    Kazutaka Matsuda

    Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020　456-483　2020

    Publisher: Springer International Publishing

    DOI： 10.1007/978-3-030-44914-8_17 　

    ISSN： 0302-9743

    eISSN： 1611-3349

    More details Close

    <title>Abstract</title>Bernardy et al. [2018] proposed a linear type system <inline-formula><alternatives><tex-math>$$\lambda ^q_\rightarrow $$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msubsup> <mml:mi>λ</mml:mi> <mml:mo>→</mml:mo> <mml:mi>q</mml:mi> </mml:msubsup> </mml:math></alternatives></inline-formula> as a core type system of Linear Haskell. In the system, linearity is represented by annotated arrow types <inline-formula><alternatives><tex-math>$$A \rightarrow _m B$$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>A</mml:mi> <mml:msub> <mml:mo>→</mml:mo> <mml:mi>m</mml:mi> </mml:msub> <mml:mi>B</mml:mi> </mml:mrow> </mml:math></alternatives></inline-formula>, where <italic>m</italic> denotes the multiplicity of the argument. Thanks to this representation, existing non-linear code typechecks as it is, and newly written linear code can be used with existing non-linear code in many cases. However, little is known about the type inference of <inline-formula><alternatives><tex-math>$$\lambda ^q_\rightarrow $$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msubsup> <mml:mi>λ</mml:mi> <mml:mo>→</mml:mo> <mml:mi>q</mml:mi> </mml:msubsup> </mml:math></alternatives></inline-formula>. Although the Linear Haskell implementation is equipped with type inference, its algorithm has not been formalized, and the implementation often fails to infer principal types, especially for higher-order functions. In this paper, based on <sc>OutsideIn(X)</sc> [Vytiniotis et al., 2011], we propose an inference system for a rank 1 qualified-typed variant of <inline-formula><alternatives><tex-math>$$\lambda ^q_\rightarrow $$</tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msubsup> <mml:mi>λ</mml:mi> <mml:mo>→</mml:mo> <mml:mi>q</mml:mi> </mml:msubsup> </mml:math></alternatives></inline-formula>, which infers principal types. A technical challenge in this new setting is to deal with ambiguous types inferred by naive qualified typing. We address this ambiguity issue through quantifier elimination and demonstrate the effectiveness of the approach with examples.

  7. Sparcl: a language for partially-invertible computation. Peer-reviewed

    Kazutaka Matsuda, Meng Wang

    Proc. ACM Program. Lang.　4　(ICFP)　118-31　2020

    DOI： 10.1145/3409000 　

  8. Embedding invertible languages with binders: a case of the FliPpr language Peer-reviewed

    Kazutaka Matsuda, Meng Wang

    Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell　158-171　2018/09/17

    Publisher: ACM

    DOI： 10.1145/3242744.3242758 　

  9. 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

  10. HOBiT: Programming lenses without using lens combinators Peer-reviewed

    Kazutaka Matsuda, Meng Wang

    Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Lecture Notes in Computer Science 10801　10801　31-59　2018

    Publisher: Springer Verlag

    DOI： 10.1007/978-3-319-89884-1_2 　

    ISSN： 1611-3349 0302-9743

  11. Applicative bidirectional programming: Mixing lenses and semantic bidirectionalization. Peer-reviewed

    Kazutaka Matsuda, Meng Wang

    J. Funct. Program.　28　e15　2018

    DOI： 10.1017/S0956796818000096 　

  12. FliPpr: A System for Deriving Parsers from Pretty-Printers Peer-reviewed

    Kazutaka Matsuda, Meng Wang

    New Generation Computing　36　(3)　173-202　2018

    DOI： 10.1007/s00354-018-0033-7 　

  13. 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 2017　71-82　2017

    DOI： 10.1145/3018882.3018883 　

  14. "Bidirectionalization for free" for monomorphic transformations Peer-reviewed

    Kazutaka Matsuda, Meng Wang

    Science of Computer Programming　111　79-109　2015/11

    DOI： 10.1016/j.scico.2014.07.008 　

    ISSN： 0167-6423

    eISSN： 1872-7964

  15. Trace-based Approach to Editability and Correspondence Analysis for Bidirectional Graph Transformations Peer-reviewed

    Soichiro Hidaka, Martin Billes, Quang Minh Tran, Kazutaka Matsuda

    Proceedings of the 4th International Workshop on Bidirectional Transformations co-located with Software Technologies: Applications and Foundations, STAF 2015　2015/07

  16. Applicative Bidirectional Programming with Lenses Peer-reviewed

    Kazutaka Matsuda, Meng Wang

    PROCEEDINGS OF THE 20TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING (ICFP'15)　62-74　2015

    DOI： 10.1145/2784731.2784750 　

  17. Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking Peer-reviewed

    Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda

    CONCUR 2014 – Concurrency Theory, Lecture Notes in Computer Science 8704　312-326　2014

    Publisher: Springer Berlin Heidelberg

    DOI： 10.1007/978-3-662-44584-6_22 　

    ISSN： 0302-9743

    eISSN： 1611-3349

  18. Refactoring pattern matching Peer-reviewed

    Meng Wang, Jeremy Gibbons, Kazutaka Matsuda, Zhenjiang Hu

    Science of Computer Programming　78　(1)　2216-2242　2013/11

    DOI： 10.1016/j.scico.2012.07.014 　

  19. Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins Peer-reviewed

    Janis Voigtländer, Zhenjiang Hu, Kazutaka Matsuda, Meng Wang

    Journal of Functional Programming　23　(5)　515-551　2013/09

    DOI： 10.1017/S0956796813000130 　

    ISSN： 0956-7968 1469-7653

  20. FliPpr: A Prettier Invertible Printing System Peer-reviewed

    Kazutaka Matsuda, Meng Wang

    Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Lecture Notes in Computer Science 7792　7792　101-120　2013

    DOI： 10.1007/978-3-642-37036-6_6 　

    ISSN： 0302-9743

  21. Bidirectionalization for free with runtime recording: Or, a light-weight approach to the view-update problem Peer-reviewed

    Kazutaka Matsuda, Meng Wang

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

    DOI： 10.1145/2505879.2505888 　

  22. Functional programs as compressed data Peer-reviewed

    Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi

    Higher-Order and Symbolic Computation　25　(1)　39-84　2012/03/01

    Publisher: Kluwer Academic Publishers

    DOI： 10.1007/s10990-013-9093-z 　

    ISSN： 1388-3690

  23. Polynomial-time inverse computation for accumulative functions with multiple data traversals Peer-reviewed

    Kazutaka Matsuda, Kazuhiro Inaba, Keisuke Nakano

    Higher-Order and Symbolic Computation　25　(1)　3-38　2012/03/01

    Publisher: Kluwer Academic Publishers

    DOI： 10.1007/s10990-013-9097-8 　

    ISSN： 1388-3690

  24. Three Complementary Approaches to Bidirectional Programming Peer-reviewed

    Nate Foster, Kazutaka Matsuda, Janis Voigtländer

    nternational Spring School, SSGIP 2010, Oxford, UK, March 22-26, 2010, Revised Lectures, Lecture Notes in Computer Science 7470　1-46　2012

    Publisher: Springer Berlin Heidelberg

    DOI： 10.1007/978-3-642-32202-0_1 　

    ISSN： 0302-9743

    eISSN： 1611-3349

  25. Marker-Directed Optimization of UnCAL Graph Transformations Peer-reviewed

    Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Kazutaka Matsuda, Keisuke Nakano, Isao Sasano

    Logic-Based Program Synthesis and Transformation - 21st International Symposium, LOPSTR 2011, Odense, Denmark, July 18-20, 2011. Revised Selected Papers. Lecture Notes in Computer Science 7225　123-138　2012

    Publisher: Springer Berlin Heidelberg

    DOI： 10.1007/978-3-642-32211-2_9 　

    ISSN： 0302-9743

    eISSN： 1611-3349

  26. Functional programs as compressed data Peer-reviewed

    Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara

    Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM 2012　2012/01

  27. Polynomial-time inverse computation for accumulative functions with multiple data traversals Peer-reviewed

    Kazutaka Matsuda, Kazuhiro Inaba, Keisuke Nakano

    Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM 2012　2012/01

  28. Combining Syntactic and Semantic Bidirectionalization Peer-reviewed

    Janis Voigtlaender, Zhenjiang Hu, Kazutaka Matsuda, Meng Wang

    ICFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING　181-192　2010

  29. Bidirectionalizing Graph Transformations Peer-reviewed

    Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Kazutaka Matsuda, Keisuke Nakano

    ICFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING　205-216　2010

  30. Gradual Refinement Blending Pattern Matching with Data Abstraction Peer-reviewed

    Meng Wang, Jeremy Gibbons, Kazutaka Matsuda, Zhenjiang Hu

    MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS　6120　397-+　2010

    DOI： 10.1007/978-3-642-13321-3_22 　

    ISSN： 0302-9743

  31. A Grammar-Based Approach to Invertible Programs Peer-reviewed

    Kazutaka Matsuda, Shin-Cheng Mu, Zhenjiang Hu, Masato Takeichi

    PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS　6012　448-+　2010

    DOI： 10.1007/978-3-642-11957-6_24 　

    ISSN： 0302-9743

  32. Bidirectionalizing Structural Recursion on Graphs

    Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Kazutaka Matsuda, Keisuke Nakano

    日本ソフトウェア科学会第26回大会 , 島根大学（松江キャンパス）, 2009年9月16日(水)～18日(金)　2009/09

  33. 補関数の生成による複製機能付きプログラムの自動双方向化 Peer-reviewed

    松田一孝, 胡振江, 中野圭介, 浜名誠, 武市正人

    コンピュータ・ソフトウェア　26　(2)　56-75　2009/04/24

    Publisher: Japan Society for Software Science and Technology

    DOI： 10.11309/jssst.26.2_56 　

    ISSN： 0289-6540

    More details Close

    A bidirectional transformation consists of a pair of unidirectional transformations: a forward transformation that maps one data structure called source to another called view, and a backward transformation that reflects changes in the view to the source. Bidirectional transformation has many useful applications such as replicated data synchronization, presentation-oriented editor development, and software artifact synchronization. In a previous work, we proposed a framework in which a backward transformation is automatically generated from a forward transformation by derivation of a complementary function if the forward transformation is given by a program in a simple functional language. However, the language has a severe restriction that no variable is allowed to be used more than once. In this paper, we show that tupling transformation relaxes this restriction, allowing us to handle a wider class of bidirectional transformations that may contain duplications.

  34. Type-based specialization of XML transformations Peer-reviewed

    Kazutaka Matsuda, Zhenjiang Hu, Masato Takeichi

    Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation, PEPM'09　61-71　2009

    DOI： 10.1145/1480945.1480955 　

  35. 補関数の生成による複製を含むプログラムの自動双方向化

    松田一孝, 胡振江, 中野圭介, 浜名誠, 武市正人

    第10回プログラミングおよびプログラミング言語ワークショップ, 仙台市 秋保温泉 緑水亭, 2008年3月5日(水)〜3月7日(金)　2008/03

  36. Bidirectionalization transformation based on automatic derivation of view complement functions Peer-reviewed

    Kazutaka Matsuda, Zhenjiang Hu, Keisuke Nakano, Makoto Hamana, Masato Takeichi

    ACM SIGPLAN NOTICES　42　(9)　47-58　2007/09

    ISSN： 0362-1340

  37. Bidirectionalization Transformation Based on Automatic Derivation of View Complement Functions Peer-reviewed

    Kazutaka Matsuda, Zhenjiang Hu, Keisuke Nakano, Makoto Hamana, Masato Takeichi

    ICFP'07 PROCEEDINGS OF THE 2007 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING　47-58　2007

    DOI： 10.1145/1291220.1291162 　

  38. A Web service architecture for bidirectional XML updating Peer-reviewed

    Yasushi Hayashi, Dongxi Liu, Kento Emoto, Kazutaka Matsuda, Zhenjiang Hu, Masato Takeichi

    ADVANCES IN DATA AND WEB MANAGEMENT, PROCEEDINGS　4505　721-+　2007

    ISSN： 0302-9743

  39. 木上の双方向変換を利用したファイルマネージャの実現 Peer-reviewed

    松田一孝, 大川徳之, 野村芳明, 森田直幸, 筧一彦, 胡振江, 武市正人

    情報処理学会論文誌：トランザクション「プログラミング」　47　(SIG2 (PRO28))　84-98　2006/02/15

    Publisher: Information Processing Society of Japan (IPSJ)

    ISSN： 1882-7802

    More details Close

    File management is sometimes confusing due to the difference between files and their shortcuts (or symbolic links). While deleting shortcuts to a file can leave the file entity as it is, deleting a file entity may lead to dangling shortcuts. To resolve this problem, we apply the technique of bidirectional tree transformations to design and implement a new file manager which can treat file references in a symmetric and uniform way. This file manager is unique in its synchronization mechanism which eliminates the confusing difference of file references. Plural file references are synchronized, and changes applied on one reference will propagate to the others. For example, if one of the synchronized file references is deleted, the rest are also deleted automatically. This synchronization mechanism can be efficiently implemented based on bidirectional tree transformations. In this paper, we show the design and the implementation of our file manager. The interactive graphical user interface of our file manager enables us to manipulate file references easily, in which bidirectional tree transformations can produce complicated dependency.

  40. データマイニングのアルゴリズム記述を容易にする拡張行列演算の提案 Peer-reviewed

    松田一孝, 筧一彦, 胡振江, 武市正人

    情報処理学会論文誌：トランザクション「プログラミング」　46　(SIG11 (PRO26))　1-15　2005/08/15

    Publisher: Information Processing Society of Japan (IPSJ)

    ISSN： 1882-7802

    More details Close

    The increase of machine power and the existence of the concomitant huge-sized database have made knowledge discovery and data mining possible and more important. Processing such massive date requires huge computational power and memory as well, which calls for distributed and parallel treatments. Although there have been many case studies of paral-lelizing data mining algorithms in ad hoc manners, describing parallel and distributed data mining algorithms is still a hard task. In this paper, we propose a framework, called extended matrix operations, for describinig parallel and distributed data mining algorithms in a general and uniform way. This framework is a generalization of matrix operations whose operators of addition and multiplication are generalized. This framework has the following advantages : analogy to usual matrix operations makes intuitive and concise description of algorithms; user can implement many algorithms through giving proper definitions of the generalized operators; limited number of computation patterns makes algebraic treatments of programs easy. Matrix operations have a large number of researchs on parallelization, which also apply to our framework. We explain the framework and demonstrate how concisely data miming algorithms are described in our framework. Effectiveness of our framework is examined by experiments.

Show all ︎Show first 5

Misc. 3

  1. ビブリオ・トーク -私のオススメ-：To Mock a Mocking Bird And Other Logic Puzzles : Including An Amazing Adventure in Combinatory Logic

    松田 一孝

    情報処理　56　(2)　200-201　2015/01/15

    Publisher: 一般社団法人情報処理学会

    ISSN： 0447-8053

  2. 高談闊論：双方向変換の原理と実践

    加藤 弘之, 胡 振江, 日高 宗一郎, 松田一孝

    Computer Software　2014/05

  3. Construction of Bidirectional Programs with Complementary Functions(<Series>Quick Report on Doctoral Theses Recommended by IPSJ SIGs)

    MATSUDA Kazutaka

    IPSJ Magazine　51　(10)　1362-1362　2010/10/15

    Publisher: Information Processing Society of Japan (IPSJ)

    ISSN： 0447-8053

Books and Other Publications 1

  1. IT研究者のひらめき本棚 : ビブリオ・トーク : 私のオススメ

    情報処理学会会誌編集委員会

    近代科学社　2017/09

    ISBN: 9784764905481

Presentations 29

  1. 先送りレンズ

    松田一孝, Minh Nguyen, Meng Wang

    日本ソフトウェア科学会第 41 回大会　2024/09/12

  2. Embedding by Unembedding Invited

    Kazutaka Matsuda, Samantha Frohlich, Meng Wang, Nicolas Wu

    日本ソフトウェア科学会第41回大会　2024/09/11

  3. OCamlにおけるEmbedding by Unembedding

    類家 健永, 松田 一孝

    第26回プログラミングおよびプログラミング言語ワークショップ　2024/03/06

  4. 双方向変換言語におけるpin演算子の有用性の確認

    渡邉 進太郎, 松田 一孝

    第26回プログラミングおよびプログラミング言語ワークショップ　2024/03/05

  5. Lenses for Web Applications

    Zihang Ye, Kazutaka Matsuda

    プログラミングおよびプログラミング言語ワークショップ　2023/03/06

  6. Kalpis: An Arrow Metalanguage for Partially Invertible Computation

    Anders Ågren Thuné, Kazutaka Matsuda, Meng Wang

    プログラミングおよびプログラミング言語ワークショップ　2023/03/06

  7. Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches

    Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

    2022/03/08

  8. Sparcl: A Language for Partially-Invertible Computation

    Kazutaka Matsuda, Meng Wang

    2021/03/09

  9. Modular Inference of Linear Types for Multiplicity-Annotated Arrows Invited

    Kazutaka Matsuda

    日本ソフトウェア科学会第37回大会　2020/09/08

  10. High-Level Language for Bidirectional Transformations: Experiences and Future Directions Invited

    Kazutaka Matsuda

    SFDI2020: Fourth Workshop on Software Foundations for Data Interoperability　2020/09/05

  11. Linear Quipper: 埋め込み線形型付き量子プログラミング言語

    菅野翔太, 松田一孝

    日本ソフトウェア科学会第35回大会　2018/08

  12. 負型と分数型を持つ線形型付き可逆プログラミング言語とその並行計算に基づく意味論

    八木颯, 松田一孝

    日本ソフトウェア科学会第 35 回大会　2018/08

  13. HOBiT: A Higher-Order Language that Bridges Uni- and Bi-directional Programming

    Kazutaka Matsuda, Meng Wang

    2016/09

  14. 関数型プログラムの不変条件のICE流学習手法

    千葉知也, 佐藤亮介, 松田一孝, 小林直樹

    日本ソフトウェア科学会第32回大会　2015/09

  15. Applicative Bidirectional Programming with Lenses Invited

    Kazutaka Matsuda, Meng Wang

    2015/09

  16. RePair流高階圧縮アルゴリズムの最適化

    武田広太郎, 小林直樹, 松田一孝

    日本ソフトウェア科学会第31回大会　2014/09

  17. FliPpr: A Prettier Invertible Printing System International-presentation

    Kazutaka Matsuda, Meng Wang

    10th Asian Symposium on Programming Languages and Systems　2012/12

  18. Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals International-presentation

    Kazutaka Matsuda, Kazuhiro Inaba, Keisuke Nakano

    1st International Workshop on Trends in Tree Automata and Tree Transducers　2012

  19. Towards State-based Interface to a Graph Roundtrip Transformation System GRoundTram

    Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Kazutaka Matsuda, Keisuke Nakano

    2010/11/30

  20. マクロ木変換器の多項式時間逆実行

    松田一孝, 中野圭介, 稲葉一浩

    第12回プログラミングおよびプログラミング言語ワークショップ　2010/03/03

  21. PaI: A Grammar-Based Program Inversion System International-presentation

    Kazutaka Matsuda

    The Seventh Asian Symposium on Programming Languages and Systems　2009/12/14

  22. ガイド付き木オートマトンに基づく逆プログラムの自動生成

    松田一孝, 穆信成, 胡振江, 武市正人

    日本ソフトウェア科学会第26回大会　2009/09/16

  23. 木文法の構文解析を利用したプログラム逆計算

    松田一孝, 胡振江, 武市正人, 穆信成

    第11回プログラミングおよびプログラミング言語ワークショップ　2009/03/09

  24. 補関数の生成に基づく森上の変換の双方向化

    松田一孝, 胡振江, 武市正人

    日本ソフトウェア科学会第25回大会　2008/09/10

  25. 補関数の生成による複製を含むプログラムの自動双方向化

    松田一孝, 胡振江, 中野圭介, 浜名誠, 武市正人

    第10回プログラミングおよびプログラミング言語ワークショップ　2008/03/05

  26. 木構造データに対するビュー更新反映プログラムの自動生成

    松田一孝, 胡振江, 中野圭介, 浜名誠, 武市正人

    第9回プログラミングおよびプログラミング言語ワークショップ　2007/03/08

  27. 木上の双方向変換を利用したファイルマネージャの実現

    松田一孝, 胡振江, 武市正人

    第８回プログラミングおよびプログラミング言語ワークショップ　2006/03/05

  28. A Domain Specific Language for Knowledge Discovery based on Dual Computations International-presentation

    Kazutaka Matsuda

    The Second ASIAN Symposium on Programming Languages and Systems　2004/11/04

  29. 階層的分割による並列連想計算

    松田一孝, 西岡真吾, 胡振江, 武市正人

    日本ソフトウェア科学会第21回大会　2004/09/15

Show all Show first 5

Research Projects 13

  1. High-Level Bidirectional-Transformation-Network Programming Langauge for Synchronization of Multiple Data

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research

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

    Institution: Tohoku University

    2022/04 - 2027/03

  2. 一方向プログラミングと双方向プログラミングの融合

    松田 一孝

    Offer Organization: 日本学術振興会

    System: 科学研究費助成事業 基盤研究(C)

    Category: 基盤研究(C)

    Institution: 東北大学

    2019/04 - 2023/03

    More details Close

    本研究の目的は一方向プログラミング技術と双方向プログラミング技術の融合により，現実的な労力での双方向プログラミングを行うことができるプログラミング言語の設計である. 可逆プログラミングは双方向プログラミングの特殊な場合の一つであり，またそれ自身が重要な問題である．これまでの可逆プログラミング言語は，可逆な処理を基本とし，それを組み合わせることによって可逆プログラムを構成していた．しかしながら，可逆な処理は単射でなければならないため制限が強く，またしばしば単純な例についても不自然なプログラミングを要求してしまう．一方で，より多くの処理が一部の引数を「固定」することにより単射となることが知られていたが，そうした部分可逆（partially invertible）な処理を基本とするようなプログラミング言語はこれまで存在していなかった． 研究代表者らは，部分可逆な処理を基本とするような線形型付き高階部分可逆プログラミング言語Sparclを提案した．この言語では，可逆に扱われるデータとそうでないデータが型によって区別されている（可逆型）．可逆型により，可逆な関数な関数を可逆型間の関数として，また部分可逆な関数をさらに可逆型でない型の引数を追加でとる関数として統一的に表現できる．また，Sparclはさらに， Sparclは可逆型の値を局所的に「固定」して普通の型の値の変換するための演算子pinを提供している．これらにより，Sparclでは可逆プログラミングを比較的自然な形で記述することが可能になっている． この研究の成果はプログラミング言語理論分野のトップレベル国際会議の一つICFP 2020に採録された．

  3. Highly-Usable High-Level Bidirectional Programming Language

    Kazutaka Matsuda

    Offer Organization: Japan Society for the Promotion of Science

    System: JSPS Bilateral Joint Research Projects

    2019/04 - 2021/03

  4. 双方向変換記述のための高水準プログラミング言語

    松田一孝

    Offer Organization: 栢森情報科学振興財団

    System: 研究助成

    Institution: 東北大学

    2018/01 - 2021/03

  5. New reational program semantics based on the notion of continuations and contexts

    Sumii Eijiro, Matsuda Kazutaka, Kiselyov Oleg

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research Grant-in-Aid for Challenging Exploratory Research

    Category: Grant-in-Aid for Challenging Exploratory Research

    Institution: Tohoku University

    2016/04 - 2019/03

    More details Close

    A theory for proving program equivalence, based on environmental bisimulations, has been developed in a foundational calculus modelling a functional programming language with the undelimited continuation operator "call/cc" (call-with-current-continuation).

  6. 双方向変換記述のための高階関数プログラミング言語 Competitive

    松田 一孝

    Offer Organization: 日本学術振興会

    System: 若手研究(B)

    2015/04 - 2019/03

  7. 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 - 2017/03

    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.

  8. Higher-Order Model Checking and its Applications

    Kobayashi Naoki, SHINOHARA Ayumi, IGARASHI Atsushi, UNNO Hiroshi, TERAUCHI Tachio, SUMII Eijiro, MATSUDA Kazutaka

    Offer Organization: Japan Society for the Promotion of Science

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

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

    2011/05 - 2016/03

    More details Close

    The main topic of this research project was higher-order model checking, which is an extension of model checking, a representative method for system verification. In 2009, Kobayashi, the leader of this project, has developed the first practical algorithm for higher-order model checking, and also shown that higher-order model checking is useful for program verification. This research project has been launched to extend his results. The major results include: the development of much faster higher-order model checkers, implementation of fully-automated tools for program verification, and applications to data compression (where data are compressed in the form of functional programs that generate them, and compressed data are manipulated without decompression).

  9. Program Inversion for m-to-1 Mutual Conversion

    MATSUDA Kazutaka

    Offer Organization: Japan Society for the Promotion of Science

    System: Grants-in-Aid for Scientific Research Grant-in-Aid for Young Scientists (B)

    Category: Grant-in-Aid for Young Scientists (B)

    Institution: The University of Tokyo

    2012/04 - 2015/03

    More details Close

    Given a program, program inversion computes another problem that takes an output of the given program and returns its corresponding output. The goal of this research project is to study program inversion methods to derive mutual conversion programs whose input/output relationship is m-to-1. The main results of this project are the following two. First, we have developed a system that takes a pretty-printing program and returns the corresponding parsing program. Second, we have extended an existing free-theorem-based method to construct a bidirectional transformation from a unidirectional transformation so that more practical transformations can be handled; here, a bidirectional transformation is a transformation together with a "backward" transformation that reflects updates on the transformed data to the original.

  10. Study on Language Foundation for Bidirectional Model Transformation

    HU Zhenjiang, HIDAKA Soichiro, KATO Hiroyuki, INABA Kazuhiro, NAKANO Keisuke, SASANO Isao, EMOTO Kento, MATSUDA Kazutaka

    Offer Organization: Japan Society for the Promotion of Science

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

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

    Institution: National Institute of Informatics

    2010/04 - 2014/03

    More details Close

    Bidirectional model transformation is useful for maintaining consistency between two models in model-driven software development. However, the lack of solid language foundation and a practical tool support for systematic development of well-behaved and efficient bidirectional model transformation prevent it from being widely used. We solve this problem by proposing a novel bidirectional graph transformation language UnQL+ which is an extension of unidirectional graph query language unQL, and implementing an integrated framework called GRoundTram, which is carefully designed and implemented for compositional development of well-behaved and efficient bidirectional model transformations in UnQL. GRoundTram is equipped with a user-friendly language for coding bidirectional model transformation, a novel tool for validating both models and bidirectional model transformations, an optimization mechanism for improving efficiency, and a powerful debugging environment.

  11. Grammar-based Approach to Program Bidirectionalization Competitive

    MATSUDA Kazutaka

    Offer Organization: Japan Society for the Promotion of Science

    System: Grant-in-Aid for Research Activity Start-up

    Category: Grant-in-Aid for Research Activity Start-up

    Institution: Tohoku University

    2010/04 - 2012/03

    More details Close

    Bidirectional transformations, while they have wide-ranged applications, are hard to develop because we have to maintain programs in both directions. An approach to the problem is bidirectionalization, a program transformation that constructs a bidirectional transformation from a given usual unidirectional transformation. Making use of the techniques from the formal language theory, we have developed a new fundamental technique for bidirectionalization, which enables us to enumerate all the corresponding inputs of a given output for many tree (e. g., XML)transformations in polynomial time.

  12. Advancement and Application of Type Theory for Improving Software Safety

    KOBAYASHI Naoki, IGARASHI Atsushi, SUMII Eijiro, MATSUDA Kazutaka, TERAUCHI Tachio

    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: Tohoku University

    2008 - 2010

    More details Close

    This research project aimed to improve the reliability of computer software, by refining type-based program verification methods we have studied before, and also by inventing new program verification techniques. As the former study, we have constructed verification tools for C programs and cryptographic protocols. As the latter study, we have shown novel applications of higher-order model checking to program verification, and constructed the first higher-order model checker in the world.

  13. プログラムの系統的な自動双方向化の理論と実装に関する研究

    松田 一孝

    Offer Organization: 日本学術振興会

    System: 科学研究費助成事業

    Category: 特別研究員奨励費

    Institution: 東京大学

    2008 - 2009

    More details Close

    あるデータを別のデータへと変換する,このとき変換後のデータに加えた変更を,対応するように元のデータに書き戻せると便利である.本研究は,あるデータから別データへと変換するプログラムから,変換後のデータ上の変更を元のデータに書き戻すプログラムを自動的かつ系統的に導出すること,すなわちプログラムの双方向化を目指している. プログラムの双方向化において,もし変換プログラムが単射であるならば,書き戻しプログラム導出は,変換プログラムの逆関数を導出すること(プログラム逆化)により行える.また変換プログラムが単射でない場合においても,プログラムの逆化を利用することで書き戻しプログラムを得る手法が知られている,したがってプログラムの逆化の議論はプログラムの双方向化において重要である.しかし,一般にはプログラムの逆化は容易ではない.我々はこの問題に対し,形式文法に基づくプログラム逆化手法を提案した.本手法は,既存のプログラム逆化手法と比較して,(1)拡張性の高いこと,(2)系統的であり発見的でないこと,(3)逆化可能なプログラムの特徴付けが明瞭であることの三点の特長を持つ.拡張性はより広範なプログラムを逆化する上で重要であり,手法が系統的であることと逆化可能なプログラムの特徴付けが明瞭であることは本手法をプログラムの双方向化に応用するにあたって重要である.我々は本手法の実装も行い,いくつかの例について本手法を適用することで本手法の有用性を確認した.

Show all Show first 5

Teaching Experience 6

  1. プログラミング演習B　東北大学

  2. ソフトウェア基礎科学/ソフトウエア基礎　東北大学

  3. 創造工学研修（楽しく学ぼう関数プログラミング）

  4. 情報論理学　東北大学

  5. コンパイラ実験　東京大学

  6. 関数・論理型プログラミング実験　東京大学

Show all Show first 5