研究者詳細

顔写真

マツダ　カズタカ
松田　一孝
Kazutaka Matsuda
所属
大学院情報科学研究科　情報基礎科学専攻　ソフトウェア科学講座（ソフトウェア基礎科学分野）
職名
准教授
学位

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

委員歴 52

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

    2026年4月 ～ 継続中

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

    2025年6月 ～ 継続中

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

    2023年4月 ～ 継続中

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

    2013年4月 ～ 継続中

  • 28th International Symposium on Trends in Functional Programming (TFP 2027), PC Co-Chair

    2027年3月 ～ 2027年3月

  • 日本ソフトウェア科学会第43回大会（JSSST 2026）　プログラム副委員長

    2026年9月 ～ 2026年9月

  • 2025 miniKanren and Relational Programming Workshop (miniKanren 2025)　Program Committee Member

    2025年10月 ～ 2025年10月

  • 湘南会議 No. 231 "Bidirectional Transformations: Foundations and Applications"　オーガナイザー

    2025年5月 ～ 2025年5月

  • 26th International Symposium on Trends in Functional Programming (TFP 2025)　Program Committee Member

    2025年1月 ～ 2025年1月

  • 33rd European Symposium on Programming (ESOP 2024)　Program Committee Member

    2024年4月 ～ 2024年4月

  • 2024 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2024)　Program Committee Member

    2024年1月 ～ 2024年1月

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

    2024年 ～ 2024年

  • 17th International Symposium on Theoretical Aspects of Software Engineering (TASE 2023)　Program Committee Member

    2023年7月 ～ 2023年7月

  • 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023)　プログラム共同委員長

    2023年3月 ～ 2023年3月

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

    2019年4月 ～ 2023年3月

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

    2019年4月 ～ 2023年3月

  • Tenth International Workshop on Bidirectional Transformations (BX 2022)　Program Committee Member

    2022年7月 ～ 2022年7月

  • 23rd International Symposium on Trends in Functional Programming (TFP 2022)　Program Committee Member

    2022年3月 ～ 2022年3月

  • 26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021)　Program Committee Member

    2021年8月 ～ 2021年8月

  • Ninth International Workshop on Bidirectional Transformations (Bx 2021)　Program Committee Member

    2021年6月 ～ 2021年6月

  • 第23回プログラミングおよびプログラミング言語ワークショップ（PPL 2021）　プログラム委員

    2021年3月 ～ 2021年3月

  • 日本ソフトウェア科学会第37回大会（JSSST 2020）　プログラム副委員長

    2020年9月 ～ 2020年9月

  • 12th Conference on Reversible Computation (RC 2020)　Program Committee Member

    2020年7月 ～ 2020年7月

  • 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2020)　Program Committee Member

    2020年6月 ～ 2020年6月

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

    2018年4月 ～ 2020年3月

  • 24th ACM SIGPLAN International Conference on Functional Programming (ICFP 2019)　Program Committee Member

    2019年8月 ～ 2019年8月

  • ACM SIGPLAN Haskell Symposium 2019 (Haskell 2019)　Program Committee Member

    2019年8月 ～ 2019年8月

  • Eighth International Workshop on Bidirectional Transformations (Bx 2019)　Program Committee Member

    2019年6月 ～ 2019年6月

  • 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2019)　Program Committee Member

    2019年1月 ～ 2019年1月

  • 23rd ACM SIGPLAN International Conference on Functional Programming (ICFP 2018)　External Review Committee Member

    2018年9月 ～ 2018年9月

  • Seventh International Workshop on Bidirectional Transformations (BX 2018)　Program Committee Co-Chair

    2018年4月 ～ 2018年4月

  • 第20回プログラミングおよびプログラミング言語ワークショップ（PPL 2018）　プログラム委員

    2018年3月 ～ 2018年3月

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

    2013年4月 ～ 2018年3月

  • 9th Conference on Reversible Computation (RC 2017)　Program Committee Member

    2017年7月 ～ 2017年7月

  • 湘南会議 No. 102 "Reverse Execution in Testing–Improving Security and Reliability"　オーガナイザー

    2017年7月 ～ 2017年7月

  • 第19回プログラミングおよびプログラミング言語ワークショップ（PPL 2017）　プログラム委員

    2017年3月 ～ 2017年3月

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

    2013年4月 ～ 2017年3月

  • 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016)　External Review Committee Member

    2016年9月 ～ 2016年9月

  • 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016)　Program Committee Member

    2016年9月 ～ 2016年9月

  • 24th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2016)　Program Committee Member

    2016年9月 ～ 2016年9月

  • 第18回プログラミングおよびプログラミング言語ワークショップ（PPL 2016）　組織委員

    2016年3月 ～ 2016年3月

  • 情報処理学会第77回全国大会　プログラム委員

    2015年3月 ～ 2015年3月

  • 第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015)　組織委員長

    2015年3月 ～ 2015年3月

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

    2011年4月 ～ 2015年3月

  • 6th Conference on Reversible Computation (RC 2014)　Program Committee Member

    2014年7月 ～ 2014年7月

  • 5th Conference on Reversible Computation (RC 2013)　Program Committee Member

    2013年7月 ～ 2013年7月

  • ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM 2013)　Program Committee Member

    2013年1月 ～ 2013年1月

  • 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012)　Program Committee Member

    2012年9月 ～ 2012年9月

  • 4th Conference on Reversible Computation (RC 2012)　Program Committee Member

    2012年7月 ～ 2012年7月

  • First International Workshop on Bidirectional Transformations (BX 2012)　Program Committee Member

    2012年3月 ～ 2012年3月

  • 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011)　Corporate Events Coordination Chair

    2011年9月 ～ 2011年9月

  • 21st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2011)　Program Committee Member

    2011年7月 ～ 2011年7月

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

所属学協会 4

  • 電子情報通信学会

  • Association for Computing Machinery

  • 情報処理学会

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

研究キーワード 6

  • 双方向変換

  • Correctness by Construction

  • 領域特化言語

  • プログラム変換

  • 関数プログラミング

  • プログラミング言語

研究分野 2

  • 情報通信 / ソフトウェア /

  • 情報通信 / 情報学基礎論 /

受賞 1

  1. Best Paper

    2012年1月　PEPM 2012　Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals

論文 41

  1. Lenses for Partially-Specified States. 査読有り

    Kazutaka Matsuda, Minh Nguyen, Meng Wang

    Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II. Lecture Notes in Computer Science 16502　32-63　2026年4月10日

    出版者・発行元： Springer Nature Switzerland

    DOI： 10.1007/978-3-032-22723-2_2 　

    ISSN：0302-9743

    eISSN：1611-3349

  2. Reconciling Partial and Local Invertibility 査読有り

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

    出版者・発行元： Springer Nature Switzerland

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

    ISSN：0302-9743

    eISSN：1611-3349

    詳細を見る 詳細を閉じる

    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.

  3. Sparcl: A language for partially invertible computation 査読有り

    Kazutaka Matsuda, Meng Wang

    J. Funct. Program.　34　2024年

    DOI： 10.1017/s0956796823000126 　

  4. Embedding by Unembedding 査読有り

    Kazutaka Matsuda, Samantha Frohlich, Meng Wang, Nicolas Wu

    Proceedings of the ACM on Programming Languages　7　(ICFP)　1-47　2023年8月

    DOI： 10.1145/3607830 　

  5. Synbit: synthesizing bidirectional programs using unidirectional sketches 査読有り

    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 　

  6. Synbit: synthesizing bidirectional programs using unidirectional sketches 査読有り

    Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

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

    DOI： 10.1145/3485482 　

  7. Modular Inference of Linear Types for Multiplicity-Annotated Arrows 査読有り

    Kazutaka Matsuda

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

    出版者・発行元： Springer International Publishing

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

    ISSN：0302-9743

    eISSN：1611-3349

    詳細を見る 詳細を閉じる

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

  8. Sparcl: a language for partially-invertible computation. 査読有り

    Kazutaka Matsuda, Meng Wang

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

    DOI： 10.1145/3409000 　

  9. Embedding invertible languages with binders: a case of the FliPpr language 査読有り

    Kazutaka Matsuda, Meng Wang

    Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell　158-171　2018年9月17日

    出版者・発行元： ACM

    DOI： 10.1145/3242744.3242758 　

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

  11. HOBiT: Programming lenses without using lens combinators 査読有り

    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年

    出版者・発行元： Springer Verlag

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

    ISSN：1611-3349 0302-9743

  12. Applicative bidirectional programming: Mixing lenses and semantic bidirectionalization. 査読有り

    Kazutaka Matsuda, Meng Wang

    J. Funct. Program.　28　e15　2018年

    DOI： 10.1017/S0956796818000096 　

  13. FliPpr: A System for Deriving Parsers from Pretty-Printers 査読有り

    Kazutaka Matsuda, Meng Wang

    New Generation Computing　36　(3)　173-202　2018年

    DOI： 10.1007/s00354-018-0033-7 　

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

    DOI： 10.1145/3018882.3018883 　

  15. "Bidirectionalization for free" for monomorphic transformations 査読有り

    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

  16. Trace-based Approach to Editability and Correspondence Analysis for Bidirectional Graph Transformations 査読有り

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

  17. Applicative Bidirectional Programming with Lenses 査読有り

    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 　

  18. Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking 査読有り

    Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda

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

    出版者・発行元： Springer Berlin Heidelberg

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

    ISSN：0302-9743

    eISSN：1611-3349

  19. Refactoring pattern matching 査読有り

    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 　

  20. Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins 査読有り

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

    Journal of Functional Programming　23　(5)　515-551　2013年9月

    DOI： 10.1017/S0956796813000130 　

    ISSN：0956-7968 1469-7653

  21. FliPpr: A Prettier Invertible Printing System 査読有り

    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

  22. Bidirectionalization for free with runtime recording: Or, a light-weight approach to the view-update problem 査読有り

    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 　

  23. Functional programs as compressed data 査読有り

    Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi

    Higher-Order and Symbolic Computation　25　(1)　39-84　2012年3月1日

    出版者・発行元： Kluwer Academic Publishers

    DOI： 10.1007/s10990-013-9093-z 　

    ISSN：1388-3690

  24. Polynomial-time inverse computation for accumulative functions with multiple data traversals 査読有り

    Kazutaka Matsuda, Kazuhiro Inaba, Keisuke Nakano

    Higher-Order and Symbolic Computation　25　(1)　3-38　2012年3月1日

    出版者・発行元： Kluwer Academic Publishers

    DOI： 10.1007/s10990-013-9097-8 　

    ISSN：1388-3690

  25. Three Complementary Approaches to Bidirectional Programming 査読有り

    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年

    出版者・発行元： Springer Berlin Heidelberg

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

    ISSN：0302-9743

    eISSN：1611-3349

  26. Marker-Directed Optimization of UnCAL Graph Transformations 査読有り

    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年

    出版者・発行元： Springer Berlin Heidelberg

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

    ISSN：0302-9743

    eISSN：1611-3349

  27. Functional programs as compressed data 査読有り

    Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara

    Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM 2012　2012年1月

  28. Polynomial-time inverse computation for accumulative functions with multiple data traversals 査読有り

    Kazutaka Matsuda, Kazuhiro Inaba, Keisuke Nakano

    Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM 2012　2012年1月

  29. Combining Syntactic and Semantic Bidirectionalization 査読有り

    Janis Voigtlaender, Zhenjiang Hu, Kazutaka Matsuda, Meng Wang

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

  30. Bidirectionalizing Graph Transformations 査読有り

    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年

  31. Gradual Refinement Blending Pattern Matching with Data Abstraction 査読有り

    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

  32. A Grammar-Based Approach to Invertible Programs 査読有り

    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

  33. Bidirectionalizing Structural Recursion on Graphs

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

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

  34. 補関数の生成による複製機能付きプログラムの自動双方向化 査読有り

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

    コンピュータ・ソフトウェア　26　(2)　56-75　2009年4月24日

    出版者・発行元： Japan Society for Software Science and Technology

    DOI： 10.11309/jssst.26.2_56 　

    ISSN：0289-6540

    詳細を見る 詳細を閉じる

    双方向変換は，元のデータの一部を抽出し加工する順方向変換と，順方向変換で得られたデータに対する変更を元データに書き戻す逆方向変換の二つの変換から構成される．双方向変換を用いることで，XML文書の同期や相互変換を行える．さらには，双方向変換はプレゼンテーション指向の文書作成やソフトウェアエンジニアリングにも利用できる．著者らは2007年に，順方向変換を記述するプログラムが与えられたときに自動的に逆方向変換を得る系統的な手法を提案した．しかし，そこで扱われている順方向のプログラムは制限が強く，制限の一つとして変数を二度以上使用することが禁止されていたため，複製を含む変換は記述できなかった．そこで本論文では，前手法を拡張し，複製を含むプログラムにおいても自動的に逆方向変換を得る手法を提案する．

  35. Type-based specialization of XML transformations 査読有り

    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 　

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

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

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

  37. Bidirectionalization transformation based on automatic derivation of view complement functions 査読有り

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

    ACM SIGPLAN NOTICES　42　(9)　47-58　2007年9月

    ISSN：0362-1340

  38. Bidirectionalization Transformation Based on Automatic Derivation of View Complement Functions 査読有り

    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 　

  39. A Web service architecture for bidirectional XML updating 査読有り

    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

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

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

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

    出版者・発行元： 一般社団法人情報処理学会

    ISSN：1882-7802

    詳細を見る 詳細を閉じる

    ファイルの操作において，ショートカットまたはシンボリックリンクといった別名の存在は，しばしばユーザを混乱させる．初心者にとってファイル実体と別名との区別は難しい，たとえば通常のファイルマネージャでは，ファイル実体を削除してもそれを指し示している別名は消えずに残り，逆に別名を削除しただけではファイル実体は削除されない．そこで，我々はファイルへの参照すべてを対称かつ統一的に抽象化して扱うファイルマネージャを，木上の双方向変換の技術を用いて実現する．我々のファイルマネージャの上では，1 つのファイルへの複数の参照は互いに同期されており，1 つを変更すると必ず同期された別の部分に伝播される．たとえば，1 つをディレクトリ木から削除すると残りも削除される．さらに，双方向変換を利用することにより，ディレクトリ木からの情報を抽出し操作して表示するなどのディレクトリ木の"見せ方" を抽象化および拡張でき，またその"見せ方"自体も変更することができる．このような"見せ方" の操作やファイル木に対する編集操作は，GUIを通して対話的に実行することができる．本論文では，この木上の双方向変換を利用したファイルマネージャの設計とその実装とを示す．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.

  41. データマイニングのアルゴリズム記述を容易にする拡張行列演算の提案 査読有り

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

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

    出版者・発行元： 一般社団法人情報処理学会

    ISSN：1882-7802

    詳細を見る 詳細を閉じる

    計算機性能の向上およびそれにともなうデータ量の増加により，知識発見，データマイニングの重要性が高まってきている．その処理には多くのメモリ，高い演算能力が必要とされ並列分散化の必要があり，個々の問題に対しては様々な並列分散化が施されている．しかし，一般に並列分散アルゴリズムの記述を行うことは難しい．本研究では，データマイニングにおける並列分散アルゴリズムの記述を容易にすることを目的として，「拡張行列演算」と呼ぶ並列アルゴリズム記述の枠組みを提案する．この枠組みは行列演算の加算および乗算の演算子を一般化したものである．枠組みの持つ計算パターンは少ないが，行列演算のアナロジがアルゴリズム記述を容易かつ簡潔にしており，また問題に対し適切な演算子を定義することができるためそのその表現力は高い．行列計算の並列化に関する研究は多く，同様にこの枠組みの分散並列化も行うことができる．計算パターンが少ないことはプログラムの代数的な取扱いが容易となる利点も持つ．本論文では，枠組みの概要，いくつかのデータマイニングのアルゴリズム記述例を示し，実験を通してこの枠組みの有用性を示す．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 parallelizing 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.

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

MISC 5

  1. Bidirectional Transformations: Foundations and Applications 国際共著

    Kazutaka Matsuda, Romina Eramo, Michael Johnson, Vadim Zaytsev

    NII Shonan Meeting Report　231　1-31　2025年

    出版者・発行元： National Institute of Informatics

  2. Reverse Execution in Testing – Improving Security and Reliability 国際共著

    Michael Kirkedal Thomsen, Kazutaka Matsuda, Mohammad Reza Mousavi

    NII Shonan Meeting Reports　2017-9　1-12　2017年

    出版者・発行元： National Institute of Informatics

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

    松田 一孝

    情報処理　56　(2)　200-201　2015年1月15日

    出版者・発行元： 一般社団法人情報処理学会

    ISSN： 0447-8053

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

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

    コンピュータ・ソフトウェア　2014年5月

  5. 補関数によるプログラムの双方向化に関する研究(<連載>研究会推薦博士論文速報)

    松田 一孝

    情報処理　51　(10)　1362-1362　2010年10月15日

    出版者・発行元： 一般社団法人情報処理学会

    ISSN： 0447-8053

書籍等出版物 2

  1. プログラマーのための圏論

    Milewski, Bartosz, 北川, 雅裕, 松田, 一孝

    オーム社　2026年5月

    ISBN: 9784274234866

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

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

    近代科学社　2017年9月

    ISBN: 9784764905481

講演・口頭発表等 32

  1. Lenses for Partially-Specified States

    Kazutaka Matsuda, Minh Nguyen, Meng Wang

    第28回プログラミングおよびプログラミング言語ワークショップ　2026年3月9日

  2. 高階関数型部分可逆プログラミング言語における配列操作

    須藤 龍一, 松田 一孝

    第28回プログラミングおよびプログラミング言語ワークショップ　2026年3月9日

  3. Mutually-Recursive Definition Builders

    Kazutaka Matsuda

    27th International Symposium on Trends in Functional Programming　2026年1月28日

  4. 先送りレンズ

    松田一孝, Minh Nguyen, Meng Wang

    日本ソフトウェア科学会第 41 回大会　2024年9月12日

  5. Embedding by Unembedding 招待有り

    Kazutaka Matsuda, Samantha Frohlich, Meng Wang, Nicolas Wu

    日本ソフトウェア科学会第41回大会：トップカンファレンス特別講演　2024年9月11日

  6. OCamlにおけるEmbedding by Unembedding

    類家 健永, 松田 一孝

    第26回プログラミングおよびプログラミング言語ワークショップ　2024年3月6日

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

    渡邉 進太郎, 松田 一孝

    第26回プログラミングおよびプログラミング言語ワークショップ　2024年3月5日

  8. Lenses for Web Applications

    Zihang Ye, Kazutaka Matsuda

    プログラミングおよびプログラミング言語ワークショップ　2023年3月6日

  9. Kalpis: An Arrow Metalanguage for Partially Invertible Computation

    Anders Ågren Thuné, Kazutaka Matsuda, Meng Wang

    プログラミングおよびプログラミング言語ワークショップ　2023年3月6日

  10. Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches

    Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

    第24回プログラミングおよびプログラミング言語ワークショップ　2022年3月8日

  11. Sparcl: A Language for Partially-Invertible Computation

    Kazutaka Matsuda, Meng Wang

    第23回プログラミングおよびプログラミング言語ワークショップ　2021年3月9日

  12. Modular Inference of Linear Types for Multiplicity-Annotated Arrows 招待有り

    Kazutaka Matsuda

    日本ソフトウェア科学会第37回大会：トップカンファレンス特別講演　2020年9月8日

  13. High-Level Language for Bidirectional Transformations: Experiences and Future Directions 招待有り

    Kazutaka Matsuda

    SFDI2020: Fourth Workshop on Software Foundations for Data Interoperability　2020年9月5日

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

    菅野翔太, 松田一孝

    日本ソフトウェア科学会第35回大会　2018年8月

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

    八木颯, 松田一孝

    日本ソフトウェア科学会第 35 回大会　2018年8月

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

    松田一孝, Meng Wang

    日本ソフトウェア科学会第 33 回大会　2016年9月

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

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

    日本ソフトウェア科学会第32回大会　2015年9月

  18. Applicative Bidirectional Programming with Lenses 招待有り

    Kazutaka Matsuda, Meng Wang

    日本ソフトウェア科学会第32回大会：トップカンファレンス特別講演　2015年9月

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

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

    日本ソフトウェア科学会第31回大会　2014年9月

  20. FliPpr: A Prettier Invertible Printing System 国際会議

    Kazutaka Matsuda, Meng Wang

    10th Asian Symposium on Programming Languages and Systems　2012年12月

  21. Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals 国際会議

    Kazutaka Matsuda, Kazuhiro Inaba, Keisuke Nakano

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

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

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

    Eighth Asian Symposium on Programming Languages and Systems (APLAS 2010)　2010年11月30日

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

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

    第12回プログラミングおよびプログラミング言語ワークショップ　2010年3月3日

  24. PaI: A Grammar-Based Program Inversion System 国際会議

    Kazutaka Matsuda

    The Seventh Asian Symposium on Programming Languages and Systems　2009年12月14日

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

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

    日本ソフトウェア科学会第26回大会　2009年9月16日

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

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

    第11回プログラミングおよびプログラミング言語ワークショップ　2009年3月9日

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

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

    日本ソフトウェア科学会第25回大会　2008年9月10日

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

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

    第10回プログラミングおよびプログラミング言語ワークショップ　2008年3月5日

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

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

    第9回プログラミングおよびプログラミング言語ワークショップ　2007年3月8日

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

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

    第８回プログラミングおよびプログラミング言語ワークショップ　2006年3月5日

  31. A Domain Specific Language for Knowledge Discovery based on Dual Computations 国際会議

    Kazutaka Matsuda

    The Second ASIAN Symposium on Programming Languages and Systems　2004年11月4日

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

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

    日本ソフトウェア科学会第21回大会　2004年9月15日

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

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

  1. 複数データ同期のため高水準双方向変換ネットワーク記述言語

    松田 一孝

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

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

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

    研究機関：Tohoku University

    2022年4月 ～ 2027年3月

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

    松田 一孝

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

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

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

    研究機関：Tohoku University

    2019年4月 ～ 2023年3月

    詳細を見る 詳細を閉じる

    双方向変換は異なる種類の複数データ間の同期を可能にし，プログラミング言語やソフトウェア工学等の様々な分野で注目を集めている． 本プロジェクトでは主に，双方向変換の記述のためのプログラミング言語に関する二つの成果を得た．一つ目は高階関数型部分可逆プログラミング言語のSparclの設計・実装である．この言語では可逆性を保証したまま一方向の処理と可逆な処理を組み合せることが可能であり，結果，辞書式圧縮等をより自然な形で記述することを可能とする．もう一つは双方向変換合成システムSymbitの設計・実装である．このシステムは，通常の一方向プログラムと逆方向の入出力例から双方向プログラムを効果的に合成する．

  3. 利便性の高い高水準双方向プログラミング言語

    松田一孝

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

    制度名：JSPS Bilateral Joint Research Projects

    2019年4月 ～ 2022年3月

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

    松田一孝

    2019年1月 ～ 2021年3月

  5. 継続と文脈の概念にもとづく新しい関係的プログラム意味論

    住井 英二郎, 松田 一孝, キセリョーヴ オレッグ

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

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Challenging Exploratory Research

    研究種目：Grant-in-Aid for Challenging Exploratory Research

    研究機関：Tohoku University

    2016年4月 ～ 2019年3月

    詳細を見る 詳細を閉じる

    「難解な専門用語の使用はできるだけ避けるか…適宜説明を加えて」「最大300文字」との指示に従って述べる。「継続」とは、計算機プログラムを実行している途中の「残りの計算」を指す概念である。「文脈」とは、プログラム中のある部分に対し、そのまわりの部分（前者を[]という記号で置き換えた、「穴」のあるプログラム）を指す。本研究では、「継続」を扱う機能の一つであるcall/ccという演算を含む関数型（式の値を計算する「評価」以外の、いわゆる「副作用」がない）プログラムの等価性（動作の等しさ）を証明するための理論を「環境双模倣」という手法にもとづき確立し、その知見を他の研究にも活かすことができた。

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

    松田 一孝

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

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

    研究種目：Grant-in-Aid for Young Scientists (B)

    研究機関：Tohoku University

    2015年4月 ～ 2019年3月

    詳細を見る 詳細を閉じる

    双方向変換は，複数のデータ間の同期を可能とし，プログラミング言語，ソフトウェア工学，データベース等様々な分野で注目を集めている重要な研究課題である． 本プロジェクトでは，双方向変換記述のための高階関数プログラミング言語の設計を行った．この言語では，双方向変換は通常の関数として表現されるため，ユーザはその関数表現を高階関数を用いて組み合わせることでより複雑な双方向変換を記述することが可能となっている．また，束縛子を持つような双方向変換プログラミング言語の新しい埋め込み実装法を提案し，その有用性を構文解析器/整形出力器記述のための双方向言語FliPprを埋めこむことで確認した．

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

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

    提供機関：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月 ～ 2017年3月

    詳細を見る 詳細を閉じる

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

  8. 高階モデル検査とその応用

    小林 直樹, 篠原 歩, 五十嵐 淳, 海野 広志, 寺内 多智弘, 住井 英二郎, 松田 一孝

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

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

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

    2011年5月 ～ 2016年3月

    詳細を見る 詳細を閉じる

    本研究の中心テーマである高階モデル検査とは、代表的なシステム検証手法であるモデル検査の拡張であり、2009年に研究代表者の小林によって初めて現実的な高階モデル検査アルゴリズムおよびプログラム検証への応用が見出された。本研究課題はその結果を受けて行った研究であり、高階モデル検査器の大幅な高速化、高階モデル検査に基づく全自動プログラム検証器の構築、高階モデル検査のデータ圧縮への応用（データをそれを生成する関数型プログラムの形に圧縮し、圧縮したままのデータ操作を実現）などの成果を得た。

  9. 一対一でない相互変換のためのプログラム逆計算

    松田 一孝

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

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Young Scientists (B)

    研究種目：Grant-in-Aid for Young Scientists (B)

    研究機関：The University of Tokyo

    2012年4月 ～ 2015年3月

    詳細を見る 詳細を閉じる

    プログラム逆計算は，プログラムが与えられたときに，そのプログラムの出力から対応する入力を計算するプログラムを求める．本プロジェクトの目的は，プログラム逆計算による多対一の関係にある相互変換プログラムの構成である．本プロジェクトの主な成果は次の二つである．一つ目は，整形出力プログラムを入力とし，構文解析プログラムを出力するシステムの作成である．二つ目は，双方向変換──通常の変換と，変換後のデータに対する変更を元データに書き戻す逆方向変換の組──を通常の一方向の変換プログラムから構成するfree theoremに基づく手法を，より実用的な変換が扱えるように拡張したことである．

  10. 双方向モデル変換の言語的基盤技術に関する研究

    胡 振江, 日高 宗一郎, 加藤 弘之, 稲葉 一弘, 中野 圭介, 篠埜 功, 江本 健斗, 松田 一孝

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

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

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

    研究機関：National Institute of Informatics

    2010年4月 ～ 2014年3月

    詳細を見る 詳細を閉じる

    双方向モデル変換は、モデル駆動ソフトウェア開発において、従来は上流過程から下流過程への単方向のモデル変換であったものを、下流過程におけるモデルの修正を上流過程に反映させること目的としており、その言語的技術基盤を確立すべく、言語の設計、実装、応用にわたって研究するという当初の研究計画に対して、以下のような成果を挙げた。(1) 双方向グラフ変換の言語UnQL+を提案し、双方向モデル変換の基盤技術を確立した。(2) 世界初の双方向グラフ変換エンジン GRoundTram を実現し公開し、ヨーロッパやアジアのグループが研究に利用している。(3) モデルとコードの共進化に応用し、国際的な評価を得た。

  11. プログラムの形式文法に基づく双方向化の研究

    松田 一孝

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

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

    研究種目：Grant-in-Aid for Research Activity Start-up

    研究機関：Tohoku University

    2010年 ～ 2011年

    詳細を見る 詳細を閉じる

    双方向変換は, 様々な応用を持つため有用であるが, 双方向変換を手で書くのは手間でバグが入りやすい. この問題に対するアプローチの一つが双方向化であり, 通常の変換プログラムから双方向変換の導出を行う. 本研究成果として, 形式文法の知見を応用し新らたな双方向化の基盤技術を得た. 本技術を利用することにより, 多くのXML変換についてその出力が与えられたときに対応する全入力を多項式時間で求めることができるようになる.

  12. ソフトウェアの安全性向上のための型理論の深化と応用

    小林 直樹, 五十嵐 淳, 住井 英二郎, 松田 一孝, 寺内 多智弘

    提供機関：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)

    研究機関：Tohoku University

    2008年 ～ 2010年

    詳細を見る 詳細を閉じる

    本研究では, ソフトウェアの信頼性向上のため, これまで研究代表者らが提案してきた型に基づくプログラム検証手法を実用レベルに引き上げるとともに, 検証手法の開拓を目標としていた. 前者の主な成果として, Cプログラムやセキュリティプロトコルの自動検証ツールの構築が挙げられる. また, 後者の主な成果として, 高階モデル検査のプログラム検証への応用を示すとともに, 世界初の高階モデル検査器の構築に成功した.

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

    松田 一孝

    2008年 ～ 2009年

    詳細を見る 詳細を閉じる

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

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

担当経験のある科目(授業) 9

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

  2. 電気・通信・電子・情報工学実験C（教材の一部）　東北大学

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

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

  5. 情報論理学　東北大学

  6. 計算機ソフトウェア工学　東北大学

  7. 電気・通信・電子・情報工学実験D（住井・松田研究室）　東北大学

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

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

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