東北大学研究者紹介

研究者詳細

ホーム

日本語 English

マツダ　カズタカ

松田　一孝

Kazutaka Matsuda

所属

大学院情報科学研究科　情報基礎科学専攻　ソフトウェア科学講座（ソフトウェア基礎科学分野）

職名

准教授

学位

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

researchmap

https://researchmap.jp/7000000397

J-GLOBAL ID

201201002237994783

委員歴 10

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

2025年4月～継続中
日本ソフトウェア科学会プログラミング論研究会　運営委員

2024年4月～継続中
日本ソフトウェア科学会　論文誌「コンピュータソフトウェア」編集委員

2013年4月～継続中
日本ソフトウェア科学会プログラミング論研究会　PPLサマースクール2024 幹事

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

2019年4月～ 2023年3月
情報処理学会プログラミング研究会　幹事

2019年4月～ 2023年3月
情報処理学会東北支部　広報幹事

2019年4月～ 2020年3月
情報処理学会プログラミング研究会　運営委員

2013年4月～ 2018年3月
情報処理学会　論文誌「プログラミング」編集委員

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

2011年4月～ 2015年3月

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

所属学協会 4

電気情報通信学会
Association for Computing Machinery
情報処理学会
日本ソフトウェア科学会

研究キーワード 4

領域特化言語
プログラム変換
関数プログラミング
プログラミング言語

研究分野 2

情報通信 / ソフトウェア /
情報通信 / 情報学基礎論 /

受賞 1

Best Paper

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

論文 40

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.
Sparcl: A language for partially invertible computation 査読有り

Kazutaka Matsuda, Meng Wang

J. Funct. Program.　34　2024年

DOI： 10.1017/s0956796823000126 　
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 　
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 　
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 　
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.
Sparcl: a language for partially-invertible computation. 査読有り

Kazutaka Matsuda, Meng Wang

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

DOI： 10.1145/3409000 　
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 　
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
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
Applicative bidirectional programming: Mixing lenses and semantic bidirectionalization. 査読有り

Kazutaka Matsuda, Meng Wang

J. Funct. Program.　28　e15　2018年

DOI： 10.1017/S0956796818000096 　
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 　
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 　
"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
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月
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 　
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
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 　
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
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
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 　
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
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
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
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
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月
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月
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年
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年
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
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
Bidirectionalizing Structural Recursion on Graphs

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

日本ソフトウェア科学会第26回大会 , 島根大学（松江キャンパス）, 2009年9月16日(水)～18日(金)　2009年9月
補関数の生成による複製機能付きプログラムの自動双方向化査読有り

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

コンピュータ・ソフトウェア　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年に，順方向変換を記述するプログラムが与えられたときに自動的に逆方向変換を得る系統的な手法を提案した．しかし，そこで扱われている順方向のプログラムは制限が強く，制限の一つとして変数を二度以上使用することが禁止されていたため，複製を含む変換は記述できなかった．そこで本論文では，前手法を拡張し，複製を含むプログラムにおいても自動的に逆方向変換を得る手法を提案する．
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 　
補関数の生成による複製を含むプログラムの自動双方向化

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

第10回プログラミングおよびプログラミング言語ワークショップ, 仙台市秋保温泉緑水亭, 2008年3月5日(水)〜3月7日(金)　2008年3月
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
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 　
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
木上の双方向変換を利用したファイルマネージャの実現査読有り

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

情報処理学会論文誌：トランザクション「プログラミング」　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.
データマイニングのアルゴリズム記述を容易にする拡張行列演算の提案査読有り

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

情報処理学会論文誌：トランザクション「プログラミング」　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 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
高談闊論：双方向変換の原理と実践

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

コンピュータ・ソフトウェア　2014年5月
補関数によるプログラムの双方向化に関する研究(<連載>研究会推薦博士論文速報)

松田一孝

情報処理　51　(10)　1362-1362　2010年10月15日
出版者・発行元：一般社団法人情報処理学会
ISSN： 0447-8053

書籍等出版物 1

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

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

近代科学社　2017年9月

ISBN: 9784764905481

講演・口頭発表等 29

先送りレンズ

松田一孝, Minh Nguyen, Meng Wang

日本ソフトウェア科学会第 41 回大会　2024年9月12日
Embedding by Unembedding 招待有り

Kazutaka Matsuda, Samantha Frohlich, Meng Wang, Nicolas Wu

日本ソフトウェア科学会第41回大会　2024年9月11日
OCamlにおけるEmbedding by Unembedding

類家健永, 松田一孝

第26回プログラミングおよびプログラミング言語ワークショップ　2024年3月6日
双方向変換言語におけるpin演算子の有用性の確認

渡邉進太郎, 松田一孝

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

Zihang Ye, Kazutaka Matsuda

プログラミングおよびプログラミング言語ワークショップ　2023年3月6日
Kalpis: An Arrow Metalanguage for Partially Invertible Computation

Anders Ågren Thuné, Kazutaka Matsuda, Meng Wang

プログラミングおよびプログラミング言語ワークショップ　2023年3月6日
Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches

Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

第24回プログラミングおよびプログラミング言語ワークショップ　2022年3月8日
Sparcl: A Language for Partially-Invertible Computation

Kazutaka Matsuda, Meng Wang

第23回プログラミングおよびプログラミング言語ワークショップ　2021年3月9日
Modular Inference of Linear Types for Multiplicity-Annotated Arrows 招待有り

Kazutaka Matsuda

日本ソフトウェア科学会第37回大会　2020年9月8日
High-Level Language for Bidirectional Transformations: Experiences and Future Directions 招待有り

Kazutaka Matsuda

SFDI2020: Fourth Workshop on Software Foundations for Data Interoperability　2020年9月5日
Linear Quipper: 埋め込み線形型付き量子プログラミング言語

菅野翔太, 松田一孝

日本ソフトウェア科学会第35回大会　2018年8月
負型と分数型を持つ線形型付き可逆プログラミング言語とその並行計算に基づく意味論

八木颯, 松田一孝

日本ソフトウェア科学会第 35 回大会　2018年8月
HOBiT: A Higher-Order Language that Bridges Uni- and Bi-directional Programming

松田一孝, Meng Wang

日本ソフトウェア科学会第 33 回大会　2016年9月
関数型プログラムの不変条件のICE流学習手法

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

日本ソフトウェア科学会第32回大会　2015年9月
Applicative Bidirectional Programming with Lenses 招待有り

Kazutaka Matsuda, Meng Wang

日本ソフトウェア科学会第32回大会　2015年9月
RePair流高階圧縮アルゴリズムの最適化

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

日本ソフトウェア科学会第31回大会　2014年9月
FliPpr: A Prettier Invertible Printing System 国際会議

Kazutaka Matsuda, Meng Wang

10th Asian Symposium on Programming Languages and Systems　2012年12月
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年
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日
マクロ木変換器の多項式時間逆実行

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

第12回プログラミングおよびプログラミング言語ワークショップ　2010年3月3日
PaI: A Grammar-Based Program Inversion System 国際会議

Kazutaka Matsuda

The Seventh Asian Symposium on Programming Languages and Systems　2009年12月14日
ガイド付き木オートマトンに基づく逆プログラムの自動生成

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

日本ソフトウェア科学会第26回大会　2009年9月16日
木文法の構文解析を利用したプログラム逆計算

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

第11回プログラミングおよびプログラミング言語ワークショップ　2009年3月9日
補関数の生成に基づく森上の変換の双方向化

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

日本ソフトウェア科学会第25回大会　2008年9月10日
補関数の生成による複製を含むプログラムの自動双方向化

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

第10回プログラミングおよびプログラミング言語ワークショップ　2008年3月5日
木構造データに対するビュー更新反映プログラムの自動生成

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

第9回プログラミングおよびプログラミング言語ワークショップ　2007年3月8日
木上の双方向変換を利用したファイルマネージャの実現

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

第８回プログラミングおよびプログラミング言語ワークショップ　2006年3月5日
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日
階層的分割による並列連想計算

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

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

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

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

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

松田一孝

提供機関：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月
一方向プログラミングと双方向プログラミングの融合

松田一孝

2019年4月～ 2023年3月

詳細を見る詳細を閉じる

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

松田一孝

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

制度名：JSPS Bilateral Joint Research Projects

2019年4月～ 2021年3月
双方向変換記述のための高水準プログラミング言語

松田一孝

2018年1月～ 2021年3月
継続と文脈の概念にもとづく新しい関係的プログラム意味論

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

提供機関：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という演算を含む関数型（式の値を計算する「評価」以外の、いわゆる「副作用」がない）プログラムの等価性（動作の等しさ）を証明するための理論を「環境双模倣」という手法にもとづき確立し、その知見を他の研究にも活かすことができた。
双方向変換記述のための高階関数プログラミング言語競争的資金

松田一孝

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

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

2015年4月～ 2019年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月～ 2017年3月

詳細を見る詳細を閉じる

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

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

提供機関：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年に研究代表者の小林によって初めて現実的な高階モデル検査アルゴリズムおよびプログラム検証への応用が見出された。本研究課題はその結果を受けて行った研究であり、高階モデル検査器の大幅な高速化、高階モデル検査に基づく全自動プログラム検証器の構築、高階モデル検査のデータ圧縮への応用（データをそれを生成する関数型プログラムの形に圧縮し、圧縮したままのデータ操作を実現）などの成果を得た。
一対一でない相互変換のためのプログラム逆計算

松田一孝

提供機関：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に基づく手法を，より実用的な変換が扱えるように拡張したことである．
双方向モデル変換の言語的基盤技術に関する研究

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

提供機関：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) モデルとコードの共進化に応用し、国際的な評価を得た。
プログラムの形式文法に基づく双方向化の研究競争的資金

松田一孝

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

制度名：Grant-in-Aid for Research Activity Start-up

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

研究機関：Tohoku University

2010年4月～ 2012年3月

詳細を見る詳細を閉じる

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

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

提供機関：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プログラムやセキュリティプロトコルの自動検証ツールの構築が挙げられる. また, 後者の主な成果として, 高階モデル検査のプログラム検証への応用を示すとともに, 世界初の高階モデル検査器の構築に成功した.
プログラムの系統的な自動双方向化の理論と実装に関する研究

松田一孝

2008年～ 2009年

詳細を見る詳細を閉じる

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

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

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

プログラミング演習B　東北大学
ソフトウェア基礎科学/ソフトウエア基礎　東北大学
創造工学研修（楽しく学ぼう関数プログラミング）
情報論理学　東北大学
コンパイラ実験　東京大学
関数・論理型プログラミング実験　東京大学

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