Kento EMOTO's Home Page

研究内容

• 生成・検査・集約プログラミング
  We have been proposing and studying a new programming framework "Generate, Test, and Aggregate" (GTA for short) to support easy parallel programming. The framework is equipped with a programming style, namely, GTA programming style in which a programmer designs a naive parallel program by composing a Generator to produce a multiset of solution candidates, Testers to discard invalid candidates, and an Aggregator to make a summary of valid candidates. This style fits with practical combinatorial problems, and it is easy to write correct programs in this style. The framework also equipped with a theory of mechanical program transformations so that programmer's naive programs can be optimized into efficient parallel programs runnable on various parallel computation environments, e.g., Hadoop MapReduce. The combination of the GTA style and the optimization theory allows programmers to develop correct and efficient parallel programs easily.
  Research directions in this topic are (1) to study a theory of program transformation used in optimizing naively composed GTA programs, (2) to implement active libraries to provide the GTA programming to various programming languages, and (3) to solve application problems by using the GTA framework.
• スケルトン並列プログラミング
  We have been working on "Skeletal Parallelism", in which we are encouraged to build efficient parallel programs by composing ready-made components, called parallel skeletons. This style frees programmers from burdensome tasks in parallel programming. Research directions in this topic are (1) to design flexible, expressive efficient parallel skeletons, (2) to implement such skeletons on various parallel computer architectures, and (3) to study a methodology to derive efficient parallel program systematically or automatically from ones naively composed with skeletons.

研究活動

• GTALib
  我々は，GTAプログラミングを現実のプログラミング言語上に提供するために，関数型言語 Haskell で動く GTAプログラミングライブラリ 'GTALib' を実装しています．GTAプログラミングを実言語の上で検証することで，より実用的な並列プログラミングの枠組みを構築しようと試みています．
• SkeTo Project
  並列スケルトンライブラリ'助っ人' (SkeTo) を作成しています．その目的は，並列スケルトン（並列計算に良く現れるパタン）を提供し，それらを組み合わせる事で簡単に並列プログラムを作成可能にすることです．また，我々は，ライブラリにスケルトンの組み合わせを最適化する機構を実装しようと試みています．
• Sun Microsystems Laboratories との共同研究
  米Sunの研究機関Sun Labsのガイ・スティール博士 (Dr. Guy Steele) のグループとの間で、「Fortress上でのスケルトン並列プログラミング手法に基づいたライブラリ開発」に関する共同研究を行っています．その目的は，信頼できる並列プログラムの容易な開発をサポートするライブラリの実現です．成果の一部は既にFortress言語の標準ライブラリに組み込まれています．

論文一覧

Refereed Papers

1. Hideya Iwasaki, Kento Emoto, Akimasa Morihata, Kiminori Matsuzaki, Zhenjiang Hu
   Fregel: a functional domain-specific language for vertex-centric large-scale graph processing
   Journal of Functional Programming, Vol. 32, No. 2, 2022.
2. 神野 薫, 江本 健斗
   Watts-Strogatz モデルに基づく大規模ランダムグラフの分散並列生成
   コンピュータソフトウェア, Vol. 37, No. 2, pp. 34-45, 2020.
3. Kento Emoto, Fumihisa Sadahira
   A DSL for graph parallel programming with vertex subsets
   The Journal of Supercomputing, Springer, Vol. 76, No. 7, 4998-5015, 2020.
4. Masahiro Yasugi, Daisuke Muraoka, Tasuku Hiraishi, Seiji Umatani, Kento Emoto
   HOPE: A Parallel Execution Model Based on Hierarchical Omission
   Proceedings of the 48th International Conference on Parallel Processing, ICPP 2019, , ACM, pp. 77:1-77:11, 2019.
5. Kosuke Murata, Kento Emoto
   Recursion Schemes in Coq
   Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, , Springer, pp. 202--221, 2019.
6. 村田 康佑, 江本 健斗
   定理証明支援系Coqにおける不等式変形記法
   情報処理学会論文誌プログラミング（PRO）, Vol. 11, No. 4, pp. 1-12, 2018.
7. Akimasa Morihata, Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Hideya Iwasaki
   Optimizing Declarative Parallel Distributed Graph Processing by Using Constraint Solvers
   Functional and Logic Programming, 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings, , pp. 166-181, 2018.
8. Kazuhiko Kakehi, Kiminori Matsuzaki, Kento Emoto
   Efficient Parallel Tree Reductions on Distributed Memory Environments
   Scalable Computing: Practice and Experience, 2017, Vol. 18(1), pp. 1-15.
9. Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Akimasa Morihata, Hideya Iwasaki
   Think like a vertex, behave like a function! a functional DSL for vertex-centric big graph processing
   In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP2016, Nara, Japan, Setember 18-22, 2016, , pp. 200-213, ACM, 2016.
10. Kento Emoto, Frederic Loulergue, Julien Tesson
    A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
    In Proceedings of the 5th Conference on Interactive Theorem Proving (ITP 2014), , LNCS, Vol. 8558, pp. 258--274, Springer, 2014.
11. Kento Emoto, Kiminori Matsuzaki
    An Automatic Fusion Mechanism for Variable-Length List Skeletons in SkeTo
    International Journal of Parallel Programming (IJPP), Springer, 2014, Vol. 42, No. 4, pp. 546-563, 2014.
12. Yu Liu, Kento Emoto, Zhenjiang Hu
    A Generate-Test-Aggregate Parallel Programming Library
    Parallel Computing, Vol. 40, No. 2, pp. 116-135, 2014.
13. 劉 雨, 江本 健斗, 松崎 公紀, 胡 振江
    Accumulative Computation on MapReduce
    情報処理学会論文誌：プログラミング, Vol. 7, No. 1, pp. 18-27, 2014.
14. Yu Liu, Kento Emoto, Zhenjiang Hu
    A Generate-Test-Aggregate Parallel Programming Library
    In Proceedings of the 2013 International Workshop on Programming Models and Applications for Multicores and Manycores (PMAM 2013), ACM New York, pp. 71-81, 2013.
15. Kento Emoto, Sebastian Fischer, Zhenjiang Hu
    Filter-embedding Semiring Fusion for Programming with MapReduce
    Formal Aspects of Computing, Vol. 24, No. 4-6, pp. 623-645, 2012.
    
16. Kento Emoto, Hiroto Imachi
    Parallel Tree Reduction on MapReduce
    Procedia CS, Vol. 9, pp. 1827-1836, 2012.
    
17. Kento Emoto, Sebastian Fischer, Zhenjiang Hu
    Generate, Test, and Aggregate---A Calculation-based Framework for Systematic Parallel Programming with MapReduce
    21st European Symposium on Programming (ESOP 2012), Lecture Notes in Computer Science, Vol. 7211, pp. 254-273, Springer Verlag, 2012.
    
18. 江本 健斗
    Systematic Derivation of Efficient Parallel Algorithms for Generate-test-alpha Computation
    コンピュータソフトウェア, 29 (1): 159--175, 2012.
19. 松崎 公紀, 江本 健斗, 劉 雨
    正規表現マッチングの並列化とそのHadoopでの評価
    情報処理学会論文誌：プログラミング 4(4), pp. 1-11, 2011.
20. Kiminori Matsuzaki, Kento Emoto
    Lessons from Implementing the BiCGStab Method with SkeTo Library
    In Proceedings of the Fourth International Workshop on High-level Parallel Programming and Applications (HLPP 2010), pp. 15-24, ACM, 2010.
21. Kento Emoto, Zhenjiang Hu, Kazuhiko Kakehi, Kiminori Matsuzaki, Masato Takeichi
    Generators-of-generators Library with Optimization Capabilities in Fortress
    In Euro-Par 2010, Parallel Processing, Part II, Lecture Notes in Computer Science, Vol. 6272, pp. 26--37, 2010.
22. Kiminori Matsuzaki, Kento Emoto
    Implementing fusion-equipped parallel skeletons by expression templates
    In Post Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages (IFL 2009), Lecture Notes in Computer Science, Vol. 6041, pp. 72--89, 2010.
23. Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Masato Takeichi
    Domain-Specific Optimization Strategy for Skeleton Programs
    In Proceedings of 13th International European Conference on Parallel and Distributed Computing (EuroPar 2007), Lecture Notes in Computer Science 4641, pp. 705-714, Springer, 2007.
    
24. Kento Emoto, Zhenjiang Hu, Kazuhiko Kakehi, Masato Takeichi
    A Compositional Framework for Developing Parallel Programs on Two Dimensional Arrays
    International Journal of Parallel Programming (IJPP), Volume 35, Number 6, pp. 615-658, Springer, 2007.
25. Yasushi Hayashi, Dongxi Liu, Kento Emoto, Kazutaka Matsuda, Zhenjiang Hu, Masato Takeichi
    A Web Service Architecture for Bidirectional XML Updating
    Joint conference of the 9th Asia-Pacific Web Conference and the 8th International Conference on Web-Age Information Management (APWeb/WAIM 2007), pp. 721-732, Huangshan, China, June 16-18, 2007.
    
26. Kazuhiko Kakehi, Kiminori Matsuzaki, Kento Emoto
    Efficient Parallel Tree Reductions on Distributed Memory Environments
    In Fourth International Workshop on Practical Aspects of High-level Parallel Programming (PAPP 2007), part of The International Conference on Computational Science (ICCS 2007), pp. 601-608, Beijing, China, May 27-30, 2007.
27. 野村 芳明, 江本 健斗, 松崎 公紀, 胡 振江, 武市 正人
    木スケルトンによるXPathクエリの並列化とその評価
    コンピュータソフトウェア, 24 (3): 51-62, 2007.
28. Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Masato Takeichi
    Surrounding Theorem: Developing Parallel Programs for Matrix-Convolutions
    In 12th International Euro-Par Conference, Dresden, Germany, August/September 2006, Proceedings, pages 605 - 614, Lecture Notes in Computer Science 4128, 2006.
    
29. Kiminori Matsuzaki, Kento Emoto, Hideya Iwasaki, Zhenjiang Hu
    A Library of Constructive Skeletons for Sequential Style of Parallel Programming
    First International Conference on Scalable Information Systems (InfoScale 2006), Hong Kong, May 29 - June 1, 2006. Available from ACM Digital Library.
    

Presentations/Non-Refereed Papers/Technical Reports

1. 鵜狩 慧久, 江本 健斗
   指定した形の中間証明状態へ至る形式証明の自動生成を目指して～Transformerを用い た深層学習的アプローチ～
   火の国情報シンポジウム2024論文集, 鹿児島, 2024年3月13日-14日.
2. 志岐 颯駿, 江本 健斗
   VSML/VSS: テキストベース動画編集のための動画構造/装飾記述言語
   火の国情報シンポジウム2024論文集, 鹿児島, 2024年3月13日-14日.
3. 福島 央章, 江本 健斗
   大域的グラフ計算記述言語の最適化および辺集合に関する拡張
   火の国情報シンポジウム2023論文集, オンライン, 2023年3月13日-14日.
4. 田中 匠海, 江本 健斗
   並列計算量の形式的証明を伴う BSP プログラム用 Coq ライブラリ
   火の国情報シンポジウム2022論文集, オンライン, 2022年3月1日-2日.
5. 森 公哉, 江本 健斗
   定理証明支援系Coqによる持続型例外処理機構の形式化
   火の国情報シンポジウム2022論文集, オンライン, 2022年3月1日-2日.
6. Ryuichi Takakura, Kento Emoto
   Switching execution between vertex-centric computation and block-centric computation for distributed large-graph processing
   9th International Symposium on Applied Engineering and Sciences (SAES2021), online, 2021-12.
7. 八杉 昌宏, 江本 健斗, 平石 拓
   レベル付き持続型例外処理機構の設計
   日本ソフトウェア科学会第38回大会講演論文集, 東京都港区, 2021年9月1日-3日.
8. 八杉 昌宏, 村岡 大輔, 平石 拓, 馬谷 誠二, 江本 健斗
   HOPE: 階層的計算省略に基づく耐障害性を備えた並列実行モデル
   日本ソフトウェア科学会第37回大会講演論文集, 東京都港区, 2020年9月8日-10日.
9. 村田 康佑, 江本 健斗
   Coq における Hylomorphism を用いたプログラム運算の検証に向けて
   第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020) (カテゴリ1), 佐賀県嬉野市, 2020年3月2日-4日.
10. 神野 薫, 江本 健斗
    Watts-Strogatz モデルに基づく大規模ランダムグラフの分散並列生成
    日本ソフトウェア科学会第36回大会講演論文集, 東京都港区, 2019年8月27日-29日.
11. 村田 康佑, 江本 健斗
    高度な運算定理の Coq による証明とその自動化
    日本ソフトウェア科学会第36回大会講演論文集, 東京都港区, 2019年8月27日-29日.
12. 村田 康佑, 江本 健斗
    Coqを用いた高度なプログラム運算定理の検証に向けて
    第21回プログラミングおよびプログラミング言語ワークショップ (PPL 2019) (カテゴリ3), 岩手県花巻市, 2019年3月6日-8日.
13. 小西 篤志, 江本 健斗
    FregelからGraphXへのコンパイルにおけるSMTソルバを用いた不要な通信の削減
    第21回プログラミングおよびプログラミング言語ワークショップ (PPL 2019) (カテゴリ3), 岩手県花巻市, 2019年3月6日-8日.
14. 村田 康佑, 江本 健斗
    Coqにおける検証されたプログラム運算の拡張
    日本ソフトウェア科学会第35回大会講演論文集, 吹田市, 2018年8月28日-31日.
15. 中島 拓, 江本 健斗
    グラフ上の生成検査集約プログラミングの実現に向けて
    第20回プログラミングおよびプログラミング言語ワークショップ (PPL 2018) (カテゴリ3), 鳥取県米子市, 2018年3月5日-7日.
16. 村田 康佑, 江本 健斗
    Coqにおける可読性の高い形式的証明に向けて
    第20回プログラミングおよびプログラミング言語ワークショップ (PPL 2018) (カテゴリ3), 鳥取県米子市, 2018年3月5日-7日.
17. 白水 駿, 江本 健斗
    並列プログラム計算量の系統的機械証明手法の開発
    日本ソフトウェア科学会第34回大会講演論文集, 横浜市, 2017年9月19日-21日.
18. 森畑 明昌, 江本 健斗, 松崎 公紀, 胡 振江, 岩崎 英哉
    頂点主体並列グラフ処理の制約解消器による効率化
    日本ソフトウェア科学会第34回大会講演論文集, 横浜市, 2017年9月19日-21日.
19. 定平 典久, 江本 健斗
    頂点部分集合変数を備えた大規模グラフ計算用領域特化言語
    第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) (カテゴリ1), 山梨県笛吹市, 2017年3月8日-10日.
20. 中島 拓, 江本 健斗
    Spark GraphXへのFregelコンパイラ
    第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) (カテゴリ3), 山梨県笛吹市, 2017年3月8日-10日.
21. 江本 健斗, 松崎 公紀, 胡 振江, 森畑 明昌, 岩崎 英哉
    大規模グラフ並列処理のための関数型領域特化言語 Fregel とその評価
    日本ソフトウェア科学会第33回大会講演論文集, 仙台, 2016年9月6日-9日.
22. 江本 健斗, 松崎 公紀, 胡 振江, 森畑 明昌, 岩崎 英哉
    大規模グラフ並列処理のための関数型領域特化言語
    第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016)(カテゴリ1), 岡山県玉野市, 2016年3月7日-9日.
23. Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Akimasa Morihata, Hideya Iwasaki
    A Functional DSL for Large Scale Graph Processing
    Thirteenth International Symposium on Functional and Logic Programming (FLOPS 2016), Kochi, Japan, March 2016. (poster)
24. Le-Duc Tung, Kento Emoto, Zhenjiang Hu
    Shortest Regular Category-Path Queries
    Technical Report GRACE-TR-2014-03, 12 pages, GRACE Center, National Institute of Informatics,August 2014, Available from GRACE Technical Report List.
25. Kento Emoto, Kiminori Matsuzaki
    An Automatic Fusion Mechanism for Variable-Length List Skeletons in SkeTo
    Technical Report METR 2013-04, 18 pages, Department of Mathematical Engineering and Information Physics, University of Tokyo, 2013. Available from METR List 2013.
    
26. Kento Emoto, Sebastian Fischer, Zhenjiang Hu
    Generate, Test, and Aggregate---A Calculation-based Framework for Systematic Parallel Programming with MapReduce
    Technical Report METR 2011-34, 28 pages, Department of Mathematical Engineering and Information Physics, University of Tokyo, 2011. Available from METR List 2011.
    
27. 劉 雨, Sebastian Fischer, 江本 健斗, 胡 振江
    Implementing Generate-Test-and-Aggregate Algorithms on Hadoop
    日本ソフトウェア科学会第28回大会講演論文集, 那覇, 2011年9月27日-29日.
28. 江本 健斗
    An Algebraic Approach to Efficient Parallel Algorithms for Nested Reductions
    第13回プログラミングおよびプログラミング言語ワークショップ (PPL 2011)(カテゴリ1), 札幌市, 2011年3月9日-11日.
29. Kento Emoto
    Semirings for Free! ---An Algebraic Approach to Efficient Parallel Algorithms for Nested Reductions
    Presentation at the fourth DIKU-IST Workshop, Jan 10-13, 2011.
30. Kento Emoto
    An Algebraic Approach to Efficient Parallel Algorithms for Nested Reductions
    Technical Report METR 2011-01, 31 pages, Department of Mathematical Engineering and Information Physics, University of Tokyo, 2011. Available from METR List 2011.
    
31. Kento Emoto
    GoG Style Parallel Programming for Non-numeric Computation
    2nd Parallelism-Oblivious Programming (POP) Workshop, Kochi, September 9-10, 2010.
32. Kento Emoto
    Active Libraries for Parallel Programming in Fortress
    4th International Workshop on Bidirectional Transformation in Architecture-Based Component Composition, Kanagawa, Japan, March 12-14, 2010.
33. 江本 健斗, 寺田 洋介, 松崎 公紀, 胡 振江, 武市 正人
    最適値の並列探索のための Improving Value の Fortress 実装
    第12回プログラミングおよびプログラミング言語ワークショップ (PPL 2010)(カテゴリ1), 琴平温泉, 2010年3月3日-5日.
34. Kiminori Matsuzaki, Kento Emoto
    Implementing fusion-equipped parallel skeletons by expression templates
    In Draft Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages (IFL 2009), pp. 100-115, 2009.
35. 松崎 公紀, 江本 健斗
    式テンプレートによる最適化機能付き並列スケルトン
    日本ソフトウェア科学会第26回大会講演論文集, 島根大学, 2009年9月16日-18日.
36. 江本 健斗, 胡 振江, 筧 一彦, 松崎 公紀, 武市 正人
    プログラム運算に基づく最適化機能つきFortressライブラリ
    第11回プログラミングおよびプログラミング言語ワークショップ (PPL 2009)(カテゴリ3), 高山市, 2009年3月9日-11日.
37. 江本 健斗
    GCC上での並列プログラミングサポート(特集：マルチコアを活かすお手軽並列プログラミング)
    情報処理学会学会誌 情報処理, Vol. 49. No. 12, pp. 1369-1374, 2008.
38. 江本 健斗, 胡 振江, 筧 一彦, 松崎 公紀, 武市 正人
    A Generative Matrix Library in Fortress Relieves Programmers' Headache!
    日本ソフトウェア科学会第25回大会講演論文集, 筑波大学, 2008年9月10日-12日.
39. Kento Emoto, Zhenjiang Hu, Kazuhiko Kakehi, Kiminori Matsuzaki, Masato Takeichi
    Generator-based GG Fortress Library --Collection of GGs and Theories--
    Technical Report METR 2008-17, 19 pages, Department of Mathematical Engineering and Information Physics, University of Tokyo, 2008. Available from METR List 2008.
    
40. Kento Emoto, Zhenjiang Hu, Kazuhiko Kakehi, Kiminori Matsuzaki, Masato Takeichi
    Generator-based GG Fortress Library
    Technical Report METR 2008-16, 19 pages, Department of Mathematical Engineering and Information Physics, University of Tokyo, 2008. Available from METR List 2008.
    
41. Kento Emoto
    Domain-Specific Optimization Strategy for Skeleton Programs
    Workshop on Parallelism Oblivious Programming, Tokyo, July 26-27, 2007.
42. 江本 健斗, 松崎 公紀, 胡 振江, 武市 正人
    近傍要素を必要とするスケルトンプログラムの最適化
    第9回プログラミングおよびプログラミング言語ワークショップ (PPL 2007), pp. 125-139, 加賀温泉, 2007年3月8日-10日.
43. Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Masato Takeichi
    Domain-Specific Optimization for Skeleton Programs Involving Neighbor Elements
    Technical Report METR 2007-05, 29 pages, Department of Mathematical Engineering and Information Physics, University of Tokyo, 2007. Available from METR List 2007.
    
44. Kazuhiko Kakehi, Kiminori Matsuzaki, Kento Emoto, Zhenjiang Hu
    An Practicable Framework for Tree Reductions under Distributed Memory Environments
    Technical Report METR 2006-64, 21 pages, Department of Mathematical Engineering and Information Physics, University of Tokyo, 2006. Available from METR List 2006.
45. 松崎 公紀, 明石 良樹, 江本 健斗, 岩崎 英哉, 胡 振江
    助っ人：構成的な並列スケルトンによる並列プログラミングライブラリ
    日本ソフトウェア科学会第22回大会講演論文集, 東北大学, 2005年9月13日-15日
46. Kazuhiko Kakehi, Kiminori Matsuzaki, Akimasa Morihata, Kento Emoto, Zhenjiang Hu
    Parallel Dynamic Programming using Data-Parallel Skeletons
    In Proceedings of the 22nd JSSST Conference, Sep, 2005.
47. 野村 芳明, 江本 健斗, 松崎 公紀, 胡 振江, 武市 正人
    木スケルトンによるXPathクエリの並列化とその評価
    日本ソフトウェア科学会第22回大会論文集, 東北大学, 2005年9月13日-15日
48. Kento Emoto, Zhenjiang Hu, Kazuhiko Kakehi, Masato Takeichi
    A Compositional Framework for Developing Parallel Programs on Two Dimensional Arrays
    Technical Report METR2005-09, Department of Mathematical Informatics, University of Tokyo, 2005.
    
49. Zhenjiang Hu, Kento Emoto, Shin-Cheng Mu, Masato Takeichi
    Bidirectionalizing Tree Transformations
    Workshop on New Approaches to Software Construction (WNASC 2004), The University of Tokyo, Komaba, Tokyo, Japan, September 13-14, 2004. pp.3-22.
    

Thesis

1. Kento Emoto
   Homomorphism-based Structured Parallel Programming
   Graduate School of Information Science and Technology, University of Tokyo, 2009.
   

その他履歴等

履歴のページ参照．