研究者詳細

顔写真

ナカノ　ケイスケ
中野　圭介
Keisuke Nakano
所属
電気通信研究所　計算システム基盤研究部門　コンピューティング情報理論研究室
職名
教授
学位

  • 博士（理学）（京都大学）

  • 修士（理学）（京都大学）

経歴 5

  • 2018年4月 ～ 継続中
    東北大学　電気通信研究所　教授

  • 2013年6月 ～ 2018年3月
    電気通信大学　大学院情報理工学研究科　准教授

  • 2012年4月 ～ 2013年5月
    電気通信大学 先端領域教育研究センター　准教授

  • 2008年3月1日 ～ 2012年3月31日
    電気通信大学 先端領域教育研究センター　特任助教

  • 2003年6月1日 ～ 2008年2月29日
    東京大学大学院情報理工学系研究科　産学官連携研究員

学歴 4

  • 京都大学　理学研究科　数学・数理解析専攻

    2000年4月 ～ 2003年5月

  • 京都大学　理学研究科　数学・数理解析専攻

    1997年4月 ～ 2000年3月

  • 東京大学　理学部　数学科

    1996年4月 ～ 1997年3月

  • 東京大学　教養学部　理科一類

    1994年4月 ～ 1996年3月

委員歴 10

  • 日本ソフトウェア科学会 プログラミング論研究会　主査

    2022年4月 ～ 2024年3月

  • 情報処理学会 プログラミング研究会　主査

    2020年4月 ～ 2022年3月

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

    2022年4月 ～ 継続中

  • 日本ソフトウェア科学会　編集委員

    2013年4月 ～ 継続中

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

    2017年4月 ～ 2020年3月

  • 情報処理学会　会員サービス部門編集委員

    2015年4月 ～ 2019年3月

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

    2013年4月 ～ 2017年3月

  • 日本ソフトウェア科学会　企画委員

    2012年4月 ～ 2016年3月

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

    2012年4月 ～ 2016年3月

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

    2009年4月 ～ 2013年3月

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

所属学協会 4

  • Institute of Electrical and Electronics Engineers (IEEE)

    2019年1月 ～ 継続中

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

  • 情報処理学会

  • Association for Computing Machinery (ACM)

研究キーワード 7

  • 定理証明支援系

  • プログラミング言語理論

  • 形式言語理論

  • プログラム変換

  • 双方向変換

  • 関数型プログラミング

  • 木トランスデューサ理論

研究分野 2

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

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

受賞 4

  1. プログラミングシンポジウム 山内奨励賞

    2018年1月　山内記念会　OCaml@p: OCaml におけるデバッグ出力機構

  2. プログラミングシンポジウム 山内奨励賞

    2014年1月　山内記念会　ジグソーパズルによる関数型プログラミング

  3. ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation: A Best Paper Award

    2012年1月　Programming committee of ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation　Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals

  4. 第20回日本ソフトウェア科学会記念大会高橋奨励賞

    2004年6月　日本ソフトウェア科学会　XMLストリーム変換の自動導出が可能なXML変換言語の設計

論文 79

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

    Keishi Hashiba, Keisuke Nakano, Kazuyuki Asada, Kentaro Kikuchi

    PEPM　43-53　2025年

    DOI： 10.1145/3704253.3706139 　

  2. Lens Laws Zoo 招待有り 査読有り

    Keisuke Nakano

    Bidirectional Collaborative Data Management　1　(1)　37-59　2024年12月12日

    出版者・発行元：

    DOI： 10.1007/978-981-97-6429-7_3 　

  3. Disproving Termination of Non-erasing Sole Combinatory Calculus with Tree Automata 国際誌 査読有り

    Keisuke Nakano, Munehiro Iwami

    Lecture Notes in Computer Science　261-275　2024年9月3日

    出版者・発行元： Springer Nature Switzerland

    DOI： 10.1007/978-3-031-71112-1_19 　

    ISSN：0302-9743

    eISSN：1611-3349

  4. Deciding Linear Height and Linear Size-To-Height Increase of Macro Tree Transducers 査読有り

    Paul Gallot, Sebastian Maneth, Keisuke Nakano, Charles Peyrat

    51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)　138:1-138:20　2024年7月

    DOI： 10.4230/LIPIcs.ICALP.2024.138 　

  5. Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)

    Keisuke Nakano, Munehiro Iwami

    2024年6月20日

    DOI： 10.48550/arXiv.2406.14305 　

  6. Deciding Linear Height and Linear Size-to-Height Increase for Macro Tree Transducers

    Paul Gallot, Sebastian Maneth, Keisuke Nakano, Charles Peyrat

    2023年7月31日

    DOI： 10.48550/arXiv.2307.16500 　

  7. Time-symmetric Turing machines for computable involutions 査読有り

    Keisuke Nakano

    215　102748-102748　2022年3月

    出版者・発行元：

    DOI： 10.1016/j.scico.2021.102748 　

    ISSN：0167-6423

  8. Bidirectional Collaborative Frameworks for Decentralized Data Management 招待有り 査読有り

    Yasuhito Asano, Yang Cao, Soichiro Hidaka, Zhenjiang Hu, Yasunori Ishihara, Hiroyuki Kato, Keisuke Nakano, Makoto Onizuka, Yuya Sasaki, Toshiyuki Shimizu, Masato Takeichi, Chuan Xiao, Masatoshi Yoshikawa

    Communications in Computer and Information Science　13-51　2022年

    出版者・発行元： Springer International Publishing

    DOI： 10.1007/978-3-030-93849-9_2 　

    ISSN：1865-0929

    eISSN：1865-0937

  9. A Tangled Web of 12 Lens Laws. 査読有り

    Keisuke Nakano

    13th International Conference on Reversible Computation (RC)　185-203　2021年

    出版者・発行元： Springer

    DOI： 10.1007/978-3-030-79837-6_11 　

  10. Idempotent Turing Machines 査読有り

    Keisuke Nakano

    46th International Symposium on Mathematical Foundations of Computer Science (MFCS)　79:1-79:18　2021年

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

    DOI： 10.4230/LIPIcs.MFCS.2021.79 　

  11. Streaming ranked-tree-to-string transducers. 査読有り

    Yuta Takahashi, Kazuyuki Asada, Keisuke Nakano

    Theoretical Computer Science　870　165-187　2021年

    DOI： 10.1016/j.tcs.2020.12.033 　

  12. On properties of B-terms 査読有り

    Mirai Ikebuchi, Keisuke Nakano

    Logical Methods in Computer Science　16　(2)　2020年6月

  13. Involutory Turing Machines 査読有り

    Keisuke Nakano

    Reversible Computation　12227　54-70　2020年

    出版者・発行元： Springer International Publishing

    DOI： 10.1007/978-3-030-52482-1_3 　

    ISSN：0302-9743

    eISSN：1611-3349

  14. Towards a Complete Picture of Lens Laws 査読有り

    Keisuke Nakano

    3rd Workshop on Software Foundations for Data Interoperability (SFDI2019+)　2019年10月

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

    Yuta Takahashi, Kazuyuki Asada, Keisuke Nakano

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

    出版者・発行元： Springer

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

  16. Toward BX-Based Architecture for Controlling and Sharing Distributed Data 査読有り

    Yasunori Ishihara, Hiroyuki Kato, Keisuke Nakano, Makoto Onizuka, Yuya Sasaki

    IEEE Second Workshop on Software Foundations for Data Interoperability (SFDI 2019)　2019年2月

  17. Flexible Framework for Data Integration and Update Propagation: System Aspect 査読有り

    Yasuhito Asano, Dennis-Florian Herr, Yasunori Ishihara, Hiroyuki Kato, Keisuke Nakano, Makoto Onizuka, Yuya Sasaki

    IEEE Second Workshop on Software Foundations for Data Interoperability (SFDI 2019)　1-5　2019年2月

    出版者・発行元：

    DOI： 10.1109/BIGCOMP.2019.8679236 　

  18. On Repetitive Right Application of B-Terms. 国際共著 査読有り

    Mirai Ikebuchi, Keisuke Nakano

    3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK　18:1-18:15　2018年7月

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

    DOI： 10.4230/LIPIcs.FSCD.2018.18 　

  19. Making View Update Strategies Programmable - Toward Controlling and Sharing Distributed Data -. 査読有り

    Yasuhito Asano, Soichiro Hidaka, Zhenjiang Hu, Yasunori Ishihara, Hiroyuki Kato, Hsiang-Shang Ko, Keisuke Nakano, Makoto Onizuka, Yuya Sasaki, Toshiyuki Shimizu,Van-Dang Tran, Kanae Tsushima, Masatoshi Yoshikawa

    CoRR　abs/1809.10357　2018年

  20. A View-based Programmable Architecture for Controlling and Integrating Decentralized Data. 査読有り

    Yasuhito Asano, Soichiro Hidaka, Zhenjiang Hu, Yasunori Ishihara, Hiroyuki Kato, Hsiang-Shang Ko, Keisuke Nakano, Makoto Onizuka, Yuya Sasaki, Toshiyuki Shimizu, Kanae Tsushima, Masatoshi Yoshikawa

    CoRR　abs/1803.06674　2018年

  21. Towards practical typechecking for macro forest transducers 査読有り

    Kazuhiro Abe, Keisuke Nakano

    Journal of Information Processing　25　962-974　2017年12月1日

    出版者・発行元： Information Processing Society of Japan

    DOI： 10.2197/ipsjjip.25.962 　

    ISSN：1882-6652 0387-5806

  22. Bidirectional Certified Programming. 査読有り

    Daisuke Kinoshita, Keisuke Nakano

    Proceedings of the 6th International Workshop on Bidirectional Transformations co-located with The European Joint Conferences on Theory and Practice of Software, BX@ETAPS 2017, Uppsala, Sweden, April 29, 2017.　31-38　2017年4月

    出版者・発行元： CEUR-WS.org

  23. マクロ森トランスデューサの実用的な型検査に向けて

    阿部和敬, 中野圭介

    第113回プログラミング研究発表会　2017年3月

  24. 属性文法合成による関数融合の実装 査読有り

    中川涼太, 中野圭介

    第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) 予稿集　2017年3月

  25. 木から文字列への決定性トップダウン変換の等価性判定の実装 査読有り

    高橋祐多, 中野圭介

    第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) 予稿集　2017年3月

  26. On repetitive right application of B-terms.

    Mirai Ikebuchi, Keisuke Nakano

    CoRR　abs/1703.10938　2017年3月

  27. 既存のコード資産を利用した制御構文補完機構

    北原元気, 中野圭介

    第58回プログラミング・シンポジウム予稿集　2017年1月

  28. Context-preserving XQuery fusion 査読有り

    H. Kato, S. Hidaka, Z. Hu, K. Nakano, Y. Ishihara

    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE　25　(4)　916-941　2015年5月

    DOI： 10.1017/S096012951300008X 　

    ISSN：0960-1295

    eISSN：1469-8072

  29. Grammatical Frameworkにおける語彙データの自動生成

    渡邉秀隆, 中野圭介

    言語処理学会第21回年次大会論文集　836-839　2015年3月

  30. XQuery Streaming by Forest Transducers

    Shizuya Hakuta, Sebastian Maneth, Keisuke Nakano, Hideya Iwasaki

    2014 IEEE 30TH INTERNATIONAL CONFERENCE ON DATA ENGINEERING (ICDE)　abs/1311.6570　952-963　2014年

    ISSN：1084-4627

  31. XQuery Streaming by Forest Transducers 査読有り

    Shizuya Hakuta, Sebastian Maneth, Keisuke Nakano, Hideya Iwasaki

    2014 IEEE 30TH INTERNATIONAL CONFERENCE ON DATA ENGINEERING (ICDE)　952-963　2014年

    DOI： 10.1109/ICDE.2014.6816714 　

    ISSN：1084-4627

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

    Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

    ACM SIGPLAN NOTICES　48　(9)　305-318　2013年9月

    DOI： 10.1145/2500365.2500608 　

    ISSN：0362-1340

    eISSN：1558-1160

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

    Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

    第15回プログラミングおよびプログラミング言語ワークショップ (PPL2013) 予稿集　2013年3月

  34. JavaScript 仮想機械におけるQuickeningの効果 査読有り

    高田祥, 鵜川始陽, 中野圭介, 岩崎英哉

    第15回プログラミングおよびプログラミング言語ワークショップ (PPL2013) 予稿集　2013年3月

  35. Metamorphism in jigsaw 査読有り

    Keisuke Nakano

    Journal of Functional Programming　23　(2)　161-173　2013年3月

    DOI： 10.1017/S0956796812000391 　

    ISSN：0956-7968 1469-7653

  36. GRoundTram: An integrated framework for developing well-behaved bidirectional model transformations 査読有り

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

    Progress in Informatics　10　(10)　131-148　2013年3月

    DOI： 10.2201/NiiPi.2013.10.7 　

    ISSN：1349-8614 1349-8606

  37. ジグソーパズルによる関数型プログラミング

    中野圭介

    第54回プログラミング・シンポジウム予稿集　2013年1月

  38. A parameterized graph transformation calculus for finite graphs with monadic branches 査読有り

    Kazuyuki Asada, Soichiro Hidaka, Hiroyuki Kato, Zhenjiang Hu, Keisuke Nakano

    Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP 2013　73-84　2013年

    DOI： 10.1145/2505879.2505903 　

  39. Optimization for iterative queries on MapReduce 査読有り

    Makoto Onizuka, Hiroyuki Kato, Soichiro Hidaka, Keisuke Nakano, Zhenjiang Hu

    Proceedings of the VLDB Endowment　7　(4)　241-252　2013年

    出版者・発行元： Association for Computing Machinery

    DOI： 10.14778/2732240.2732243 　

    ISSN：2150-8097

  40. Parameterized Graph Transformation Languages with Monads

    Kazuyuki Asada, Soichiro Hidaka, Hiroyuki Kato, Zhenjiang Hu, Keisuke Nakano

    GRACE Technical Report (GRACE-TR-2012-07)　2012年10月

  41. 模倣に基づくグラフスキーマを利用したビュー更新可能性判定 査読有り

    中野圭介, 日高宗一郎, 胡振江, 稲葉一浩, 加藤弘之

    コンピュータソフトウェア　29　(2)　174-192　2012年5月

    DOI： 10.11309/jssst.29.2_174 　

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

  43. Polynomial-time inverse computation for accumulative functions with multiple data traversals

    Kazutaka Matsuda, Kazuhiro Inaba, Keisuke Nakano

    Conference Record of the Annual ACM Symposium on Principles of Programming Languages　5-14　2012年

    出版者・発行元： Association for Computing Machinery

    DOI： 10.1145/2103746.2103752 　

    ISSN：0730-8566

  44. Context-Preserving XQuery Fusion 査読有り

    Hiroyuki Kato, Soichiro Hidaka, Zhenjiang Hu, Keisuke Nakano, Yasunori Ishihara

    Mathematical Structures in Computer Science (MSCS), Cambridge University Press　916-941　2012年

  45. Marker-directed optimization of UnCAL graph transformations 査読有り

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

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)　7225　123-138　2012年

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

    ISSN：0302-9743 1611-3349

  46. Shall we juggle, coinductively? 査読有り

    Keisuke Nakano

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)　7679　(7679)　160-172　2012年

    DOI： 10.1007/978-3-642-35308-6_14 　

    ISSN：0302-9743 1611-3349

  47. Towards Bidirectional Transformations on Ordered Graphs

    Soichiro Hidaka, Kazuyuki Asada, Hiroyuki Kato, Keisuke Nakano, Zhenjiang Hu

    Technical Report, GRACE Center, National Institute of Informatics (GRACE-TR-2011-07)　2011年12月

  48. 漸進的グラフビュー維持の枠組みの提案

    加藤弘之, 鬼塚真, 日高宗一郎, 中野圭介, 胡振江

    日本ソフトウェア科学会第28 回大会 講演論文集　2011年9月

  49. 模倣に基づくグラフスキーマを利用したビュー更新可能性判定 査読有り

    中野圭介, 日高宗一郎, 胡振江, 加藤弘之

    第13回プログラミングおよびプログラミング言語ワークショップ論文集　146-160　2011年3月

  50. GRoundTram: An integrated framework for developing well-behaved bidirectional model transformations 査読有り

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

    2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings　480-483　2011年

    DOI： 10.1109/ASE.2011.6100104 　

  51. Toward bidirectionalization of ATL with GRoundTram 査読有り

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

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)　6707　(6707)　138-151　2011年

    DOI： 10.1007/978-3-642-21732-6_10 　

    ISSN：0302-9743 1611-3349

  52. Graph-Transformation Verification using Monadic Second-Order Logic 査読有り

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

    PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING　17-28　2011年

    DOI： 10.1145/2003476.2003482 　

  53. Bidirectionalizing Graph Transformations 査読有り

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

    ACM SIGPLAN NOTICES　45　(9)　205-216　2010年9月

    DOI： 10.1145/1932681.1863573 　

    ISSN：0362-1340

    eISSN：1558-1160

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

  55. Context-preserving XQuery fusion 査読有り

    Hiroyuki Kato, Soichiro Hidaka, Zhenjiang Hu, Keisuke Nakano, Yasunori Ishihara

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)　6461　(6461)　255-270　2010年

    DOI： 10.1007/978-3-642-17164-2_18 　

    ISSN：0302-9743 1611-3349

  56. 順序を考慮にいれたXQueryの融合変換 査読有り

    加藤 弘之, 日高 宗一郎, 胡 振江, 中野 圭介, 石原 靖哲

    Webとデータベースに関するフォーラム(WebDB Forum 2009)　2009年11月

  57. Bidirectionalizing Structural Recursion on Graphs

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

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

  58. An XQuery Fusion with Preserving Document Order

    Hiroyuki Kato, Soichiro Hidaka, Zhenjiang Hu, Keisuke Nakano, Yasunori Ishihara

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

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

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

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

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

    DOI： 10.11309/jssst.26.2_56 　

    ISSN：0289-6540

    詳細を見る 詳細を閉じる

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

  60. Towards a compositional approach to model transformation for software development 査読有り

    Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

    Proceedings of the ACM Symposium on Applied Computing　468-475　2009年

    DOI： 10.1145/1529282.1529383 　

  61. Rewriting XQuery to Avoid Redundant Expressions based on Static Emulation of XML Store 査読有り

    Hiroyuki Kato, Soichiro Hidaka, Zhenjiang Hu, Yasunori Ishihara, Keisuke Nakano

    ACM SIGPLAN Workshop on Programming Language Techniques for XML (PLAN-X 2009), Savannah, Georgia, USA, January 14, 2009.　2009年1月

  62. A Compositional Approach to Bidirectional Model Transformation （共著） 査読有り

    Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

    New Ideas and Emerging Results Track of 31st International Conference on Software Engineering (ICSE 2009, NIER Track), Vancouver, Canada, May 16-24, 2009.　235-+　2009年

    DOI： 10.1109/ICSE-COMPANION.2009.5070990 　

    ISSN：0270-5257

  63. Composing Stack-Attributed Tree Transducers 査読有り

    Keisuke Nakano

    THEORY OF COMPUTING SYSTEMS　44　(1)　1-38　2009年1月

    DOI： 10.1007/s00224-008-9125-y 　

    ISSN：1432-4350

    eISSN：1433-0490

  64. Computing the Cost of Typechecking of Composition of Macro Tree Transducers 査読有り

    Keisuke Nakano, Sebastian Maneth

    Information and Media Technologies　4　(4)　846-856　2009年

    出版者・発行元： Information and Media Technologies 編集運営会議

    DOI： 10.11185/imt.4.846 　

    詳細を見る 詳細を閉じる

    Macro tree transducers are a classical formal model for structural-recursive tree transformation with accumulative parameters. They have recently been applied to model XML transformations and queries. Typechecking a tree transformation means checking whether all valid input trees are transformed into valid output trees, for the given regular tree languages of input and output trees. Typechecking macro tree transducers is generally based on inverse type inference, because of the advantageous property that inverse transformations effectively preserve regular tree languages. It is known that the time complexity of typechecking an n-fold composition of macro tree transducers is non-elementary. The cost of typechecking can be reduced if transducers in the composition have special properties, such as being deterministic or total, or having no accumulative parameters. In this paper, the impact of such properties on the cost of typechecking is investigated. Reductions in cost are achieved by applying composition and decomposition constructions to tree transducers. Even though these constructions are well-known, they have not yet been analyzed with respect to the precise sizes of the transducers involved. The results can directly be applied to typechecking XML transformations, because type formalisms for XML are captured by regular tree languages.

  65. Consistent Web site updating based on bidirectional transformation 査読有り

    Keisuke Nakano, Zhenjiang Hu, Masato Takeichi

    International Journal on Software Tools for Technology Transfer　11　(6)　453-468　2009年

    DOI： 10.1007/s10009-009-0124-3 　

    ISSN：1433-2779 1433-2787

  66. 3M-4 依存関係記述スキーマによる双方向XMLアプリケーションの開発(リーディングプロジェクト e-society:高信頼プログラミング言語と構造化文書変換技術,一般セッション,リーディングプロジェクト e-society)

    林康史, 劉東喜, 中野圭介, 胡振江, 武市正人

    全国大会講演論文集　70　(5)　"5-393"-"5-394"　2008年3月13日

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

  67. 3M-3 双方向変換に基づくウェブパブリッシング支援システムVu-X(リーディングプロジェクト e-society:高信頼プログラミング言語と構造化文書変換技術,一般セッション,リーディングプロジェクト e-society)

    中野圭介, 劉東喜, 林康史, 胡振江, 武市正人

    全国大会講演論文集　70　(5)　"5-391"-"5-392"　2008年3月13日

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

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

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

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

  69. Developing Bidirectional XML Applications with Bi-X

    Dongxi Liu, 林 康史, 中野圭介, 胡 振江, 武市正人

    情報処理学会第70回全国大会, 筑波大学 筑波キャンパス, 平成20年3月13日(木)〜15日(土).　2008年3月

  70. Consistent web site updating based on bidirectional transformation 査読有り

    Keisuke Nakano, Zhenjiang Hu, Masato Takeichi

    Proceedings - 10th IEEE International Symposium on Web Site Evolution, WSE 2008　45-54　2008年

    出版者・発行元： IEEE Computer Society

    DOI： 10.1109/WSE.2008.4655395 　

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

  72. 対話的データ操作による双方向変換プログラミング

    中野 圭介, 林 康史, 劉 東喜, 胡 振江, 武市 正人, 江本 健斗, 松田 一孝

    日本ソフトウェア科学会第24回大会 , 奈良先端科学技術大学院大学, 2007年9月12日(水)〜14日(金)　2007年9月

  73. 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　42　(9)　47-58　2007年

    DOI： 10.1145/1291151.1291162 　

    ISSN：0362-1340

  74. XML stream transformer generation through program composition and dependency analysis 査読有り

    S Nishimura, K Nakano

    SCIENCE OF COMPUTER PROGRAMMING　54　(2-3)　257-290　2005年2月

    DOI： 10.1016/j.scico.2004.07.001 　

    ISSN：0167-6423

    eISSN：1872-7964

  75. 構造化文書の応需計算機構

    西岡真吾, 中野圭介, 胡振江, 武市正人

    日本ソフトウェア科学会第21回大会 , 東京工業大学, 2004年9月15日〜17日　21　42-42　2004年9月

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

    DOI： 10.11309/jssstconference.21.0.42.0 　

    ISSN：1349-3515

    詳細を見る 詳細を閉じる

    PSD (Programmable Structured Documents) は構造化文書を計算可能なプログラムとして捉えることで安全な文書処理を実現する機構である. その計算の実行(評価)は文書を保持するエディタ等のプロセスとは別の外部評価器により行われるため, 評価される文書をプロセス間で授受する効率的な手段が必要となる. By-Need DOM は外部評価器が他のプロセスが保持している文書へ効率的にアクセスするための汎用の手段を与える. By-Need DOM では, 外部評価器で文書の評価が進行し文書の一部が必要となる都度その部分のみを転送するため, 実際に転送される文書量は最小限になる. 文書の部分の指定には XPath のサブセットが使用されるため, 文書データをDOM 等により保持するサーバとの親和性は高く実装も容易である. また, By-Need DOM ではPSD の外部評価器で必要となる必要最小限のアクセスメソッドのみを実装しており, シンプルであるためその移植性は高い.

  76. XML ストリーム処理器の自動導出が可能な XML 変換言語の設計 査読有り

    中野 圭介

    コンピュータソフトウェア　21　(3)　206-212　2004年

    DOI： 10.11309/jssst.21.206 　

    ISSN：0289-6540

  77. TreeCalc : Towards Programmable Structured Documents

    武市正人, 胡振江, 筧一彦, 林康史, 穆信成, 中野圭介

    日本ソフトウェア科学会第20回記念大会 , 愛知県立大学, 2003年9月16日〜19日　2003年9月

    DOI： 10.11309/jssstconference.2003.0.81.0 　

    ISSN：1349-3515

    詳細を見る 詳細を閉じる

    A Programmable Structured Document is a structured document with dynamically calculated components that can be specified by users in a functional programming language. TreeCalc isan experimental system demonstrating the notion, basing on the XML viewer and editor. The result of the expression or the table of contents is automatically updated when the user edits the document. The designer of an XML schemema can specify, in a concisedomain-specific language, how an XML document should be displayed as well as how the dynamically computed partsshould be updated.

  78. イベント駆動型文書変換器の自動生成 査読有り

    中野 圭介, 西村 進

    コンピュータソフトウェア　19　(4)　289-295　2002年

    DOI： 10.11309/jssst.19.289 　

    ISSN：0289-6540

  79. Deriving event-based document transformers from tree-based specifications 査読有り

    Keisuke Nakano, Susumu Nishimura

    Electronic Notes in Theoretical Computer Science　44　(2)　187-211　2001年6月

    DOI： 10.1016/S1571-0661(04)80927-7 　

    ISSN：1571-0661

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

MISC 25

  1. OCaml@p: OCamlにおける手軽なデバッグ出力機構

    櫻井健二, 中野圭介

    第58回プログラミング・シンポジウム予稿集　2017年1月

  2. Rubyに対するGradual typingの導入に向けて

    丹治将貴, 中野圭介, 岩崎英哉

    第58回プログラミング・シンポジウム予稿集　2017年1月

  3. Ruby on Railsにおけるテストケース自動生成の提案と実装'

    田代克也, 中野圭介, 岩崎英哉

    第93回プログラミング研究発表会　2013年3月

  4. JavaScriptにおけるプログラム変換の効果

    田村知博, 中野圭介, 鵜川始陽, 岩崎英哉

    情報処理学会夏のプログラミング・シンポジウム報告集　2011　19-26　2012年1月6日

  5. Simulation-based Graph Schema for View Updatability Checking of Graph Queries

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

    GRACE Technical Report (GRACE-TR-2011-01)　2011年5月

  6. GRoundTramによるATLの双方向化の実現

    篠埜功, HU Zhenjiang, 日高宗一郎, 稲葉一浩, 加藤弘之, 中野圭介

    日本ソフトウエア科学会大会講演論文集(CD-ROM)　28th　ROMBUNNO.7C-2　2011年

    ISSN： 1348-0901

  7. 漸進的グラフビュー更新の枠組みの提案

    加藤弘之, 鬼塚真, 日高宗一郎, 中野圭介, HU Zhenjiang

    日本ソフトウエア科学会大会講演論文集(CD-ROM)　28th　ROMBUNNO.5A-2　2011年

    ISSN： 1348-0901

  8. Towards State-based Interface to a Graph Roundtrip Transformation System GRoundTram (poster)

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

    Eighth ASIAN Symposium on Programming Languages and Systems (APLAS 2010), Shanghai, China, November 22 - December 1, 2010　2010年12月

  9. Range Analysis of Graph Transformation for Simulation-based Schema (poster)

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

    Eighth ASIAN Symposium on Programming Languages and Systems (APLAS 2010), Shanghai, China, November 22 - December 1, 2010　2010年12月

  10. Complete Validation of Graph Transformations

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

    GRACE Technical Report GRACE-TR-2010-04　2010年5月

  11. 順序を考慮に入れたXQueryの融合変換

    加藤弘之, 日高宗一郎, HU ZHENJIANG, 中野圭介, 石原靖哲

    情報処理学会シンポジウムシリーズ(CD-ROM)　2009　(3)　ROMBUNNO.3B,3　2009年11月12日

    ISSN： 1882-0840

  12. An Order-Sensitive Fusion for XQuery

    Hiroyuki Kato, Soichiro Hidaka, Zhenjiang Hu, Keisuke Nakano, Yasunori Ishihara

    Technical Report GRACE-TR-2009-04, GRACE Center, National Institute of Informatics, September 2009, 28 pages　2009年9月

    ISSN： 1884-0760

  13. Computing the Cost of Typechecking of Composition of Macro Tree Transducers (プログラミング Vol.2 No.4)

    Keisuke Nakano, Sebastian Maneth

    情報処理学会論文誌プログラミング（PRO）　2　(4)　53-63　2009年8月28日

    出版者・発行元： 情報処理学会

    ISSN： 1882-7802

    詳細を見る 詳細を閉じる

    Macro tree transducers are a classical formal model for structural-recursive tree transformation with accumulative parameters. They have recently been applied to model XML transformations and queries. Typechecking a tree transformation means checking whether all valid input trees are transformed into valid output trees, for the given regular tree languages of input and output trees. Typechecking macro tree transducers is generally based on inverse type inference, because of the advantageous property that inverse transformations effectively preserve regular tree languages. It is known that the time complexity of typechecking an n-fold composition of macro tree transducers is nonelementary. The cost of typechecking can be reduced if transducers in the composition have special properties, such as being deterministic or total, or having no accumulative parameters. In this paper, the impact of such properties on the cost of typechecking is investigated. Reductions in cost are achieved by applying composition and decomposition constructions to tree transducers. Even though these constructions are well-known, they have not yet been analyzed with respect to the precise sizes of the transducers involved. The results can directly be applied to typechecking XML transformations, because type formalisms for XML are captured by regular tree languages.Macro tree transducers are a classical formal model for structural-recursive tree transformation with accumulative parameters. They have recently been applied to model XML transformations and queries. Typechecking a tree transformation means checking whether all valid input trees are transformed into valid output trees, for the given regular tree languages of input and output trees. Typechecking macro tree transducers is generally based on inverse type inference, because of the advantageous property that inverse transformations effectively preserve regular tree languages. It is known that the time complexity of typechecking an n-fold composition of macro tree transducers is nonelementary. The cost of typechecking can be reduced if transducers in the composition have special properties, such as being deterministic or total, or having no accumulative parameters. In this paper, the impact of such properties on the cost of typechecking is investigated. Reductions in cost are achieved by applying composition and decomposition constructions to tree transducers. Even though these constructions are well-known, they have not yet been analyzed with respect to the precise sizes of the transducers involved. The results can directly be applied to typechecking XML transformations, because type formalisms for XML are captured by regular tree languages.

  14. An Algebraic Approach to Bidirectional Model Transformations

    Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

    Technical Report GRACE-TR-2008-02　2008年9月

  15. Towards Compositional Approach to Model Transformations

    Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

    Technical Report GRACE-TR-2008-01　2008年8月

  16. 3M-5 Bidirectional XML Transformation with Bi-X

    LiuDongxi, 林康史, 中野圭介, 胡振江, 武市正人

    全国大会講演論文集　70　(5)　"5-395"-"5-396"　2008年3月13日

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

    詳細を見る 詳細を閉じる

    Bi-X is an expressive bidirectional XML transformation language, featuring that one program can be executed in two directions. In one direction, a Bi-X program transforms source XML documents into target XML documents, while in the other direction, it transforms the updated target documents together with original source documents into updated source documents. In this paper, we give a summary of the language Bi-X and introduce some applications of using Bi-X.

  17. 依存関係記述スキーマによる双方向XMLアプリケーションの開発

    林康史, LIU Dongxi, 中野圭介, HU Zhenjiang, 武市正人

    情報処理学会全国大会講演論文集　70th　(5)　5.393-5.394　2008年3月13日

  18. 双方向変換に基づくウェブパブリッシング支援システムVu‐X

    中野圭介, LIU Dongxi, 林康史, HU Zhenjiang, 武市正人

    情報処理学会全国大会講演論文集　70th　(5)　5.391-5.392-392　2008年3月13日

  19. 構造化文書の依存関係記述のための拡張スキーマ

    林康史, 劉東喜, 中野圭介, LIU Dongxi, 武市正人

    日本ソフトウエア科学会大会講演論文集(CD-ROM)　24th　1B-2　2007年

    ISSN： 1348-0901

  20. 双方向変換に基づくウェブページ更新機構

    中野圭介, 森畑明昌, HU Zhenjiang, 武市正人

    日本ソフトウエア科学会大会講演論文集(CD-ROM)　23rd　4B-3　2006年

    ISSN： 1348-0901

  21. Macro Forest TransducerからのXMLストリーム処理器の自動導出

    中野圭介

    日本ソフトウエア科学会大会講演論文集(CD-ROM)　22nd　6D-3　2005年

    ISSN： 1348-0901

  22. 構造化文書の応需計算機構

    西岡真吾, 中野圭介, HU Zhenjiang, 武市正人

    日本ソフトウエア科学会大会講演論文集(CD-ROM)　21st　3D-3-42　2004年

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

    DOI： 10.11309/jssstconference.21.0.42.0 　

    ISSN： 1348-0901

    詳細を見る 詳細を閉じる

    PSD (Programmable Structured Documents) は構造化文書を計算可能なプログラムとして捉えることで安全な文書処理を実現する機構である. その計算の実行(評価)は文書を保持するエディタ等のプロセスとは別の外部評価器により行われるため, 評価される文書をプロセス間で授受する効率的な手段が必要となる. By-Need DOM は外部評価器が他のプロセスが保持している文書へ効率的にアクセスするための汎用の手段を与える. By-Need DOM では, 外部評価器で文書の評価が進行し文書の一部が必要となる都度その部分のみを転送するため, 実際に転送される文書量は最小限になる. 文書の部分の指定には XPath のサブセットが使用されるため, 文書データをDOM 等により保持するサーバとの親和性は高く実装も容易である. また, By-Need DOM ではPSD の外部評価器で必要となる必要最小限のアクセスメソッドのみを実装しており, シンプルであるためその移植性は高い.

  23. XMLストリーム処理器の自動導出が可能なXML変換言語の設計

    中野圭介

    日本ソフトウエア科学会大会論文集　20th　(Pt.2)　273-277　2003年9月16日

    ISSN： 0913-5391

  24. SOBAに基づいた共著支援システム

    伊藤徹, 香川考司, 角谷良彦, GARRIGUE J, 中野圭介, 西村進, 林良生, 中島玲二

    情報処理学会全国大会講演論文集　65th　(4)　4.1-4.2　2003年3月25日

  25. イベント駆動型文書変換器の自動生成

    中野圭介, 西村進

    日本ソフトウエア科学会大会論文集　18th　(2)　199-203　2001年9月18日

    ISSN： 0913-5391

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

書籍等出版物 1

  1. 定理証明手習い

    Daniel P. Friedman, Carl Eastlund, 中野圭介

    2017年10月

    ISBN: 9784908686023

講演・口頭発表等 3

  1. XQueryプログラムに対するMacro Forest Transducersを用いた型検査機構

    白田 靜哉, 中野 圭介, 岩崎 英哉

    第14回プログラミングおよびプログラミング言語ワークショップ（PPL2012）　2012年3月

  2. GRoundTram: An Integrated Framework for Developing Well-Behaved Bidirectional Model Transformations (short paper)

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

    26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011)　2011年11月

  3. 模倣に基づくグラフスキーマを利用したビュー更新可能性判定

    中野圭介, 日高宗一郎, 胡振江, 稲葉一浩, 加藤弘之

    第13回プログラミングおよびプログラミング言語ワークショップ (PPL2011)　2011年3月

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

  1. 物理的・確率的システムの検証を支える形式的基盤の構築

    Affeldt Reynald, J Garrigue, 勝股 審也, 溝口 佳寛, 中野 圭介, 才川 隆文

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

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

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

    研究機関：National Institute of Advanced Industrial Science and Technology

    2022年4月1日 ～ 2026年3月31日

  2. 双方向変換言語のための計算モデルとプログラミング言語への応用

    中野 圭介

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

    詳細を見る 詳細を閉じる

    双方向変換とは，異なる環境のデータ間における互いの整合性を保守するための両方向の変換のことで，データベースの同期やモデル駆動ソフトウェア開発などにおいて重要な役割を果たしている技術である． 本研究の目的は，この双方向変換を定義しやすくしたした言語（双方向変換言語）に関する二つの問題点を解決することである．初年度である令和三年度は，そのうちの一つである双方向変換言語の表現力に関して研究を進めた． 既存の双方向変換言語は，双方向変換が満たすべきラウンドトリップ性（二つの変換が互いに矛盾しないこと）を自動的に保証させるために，構文的な制約が設けられている．しかしながら，この制約のために任意の計算可能な双方向変換が記述できない可能性が指摘されている．本研究では，既存の双方向変換言語が過不足なく計算可能な双方向変換を定義できるかを確認することを目的としているため，研究期間の前半では双方向変換言語のための計算モデルを設計するという計画であった．初年度である令和三年度においては，双方向変換言語の二つの性質である対合性と冪等性についてそれぞれ計算モデルを作成した．以下では，この二つの計算モデルについて紹介する． まず，対合関数とは，逆関数が自分自身であるような関数のことで，定義域に含まれるどんな入力に対しても二度関数適用することで元に戻るような関数である．研究代表者は，時間対称チューリング機械という計算モデルを定義し，これが計算可能な対合関数を過不足なく表現できることを示すことに成功した．一方，冪等関数とは，定義域に含まれるどんな入力に対しても二度関数適用すると，一度だけの関数適用で得られる出力と同じ結果が得られるような関数である．研究代表者は，冪等チューリング機械という計算モデルを定義し，これが計算可能な冪等関数を過不足なく表現できることを示すことにも成功した．

  3. 民主的データ流通社会を実現するCDMSの基盤技術と応用に関する研究

    吉川 正俊, 浅野 泰仁, 中野 圭介, 鬼塚 真

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

    詳細を見る 詳細を閉じる

    本研究の目標である信頼性の高い自律分散環境の実現には，表現力の高い双方向変換言語が不可欠である．本年度は，一般的な双方向変換言語がもつべき表現力について計算論的アプローチによって考察し，その部分的な解として対合とよばれる関数に対する計算モデルを構築した．また，自律分散環境における更新伝播の不整合関係の検出アルゴリズムについても実装を進めた． また，時間変化するクエリワークロードの特性を捉えることで，スキーママイグレーションコストとクエリワークロードの実行コストを最小化するスキーマ最適化の研究に取り組んだ．特に，1) ワークロードを階層的に要約することで候補解を枝刈りする手法を考案し，2) 解を局所探索することにより大量クエリに対して高速に最適解を探索する手法を考案し，探索解の精度劣化を押さえながら最適化時間を1/10に削減できることを確認した． さらに，CDMSのアプリケーションとなるライドシェアリングサービスアライアンスの分散データ統合について研究し，3種類のモデル(集中型の調停者ビューモデル，非集中型のプロバイダビューモデル及びユーザビューモデル)を提案した．また，開発中の共有型実体化ビューアーキテクチャ(Dejima 1.0及びBCDS)によるこれらのモデルの実現性を明らかにした．差分プライバシを利用した分散環境における連合学習では，局所差分プライバシとシャッフルモデルを用いた手法を開発し，従来手法に比べ効用が大幅に改善することを示した．位置情報プライバシについては，利用者がどの位置同士は敵対者から区別ができないようにしたいかを示すポリシーを遵守しながら差分プライバシーを満足する手法を考案しプロトタイプを開発した．

  4. 定式化された形式木言語理論に基づくソフトウェア基盤技術の開発

    中野 圭介

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

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

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

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

    詳細を見る 詳細を閉じる

    形式木言語理論とは，形式的な木構造データを扱うことのできる木オートマトンや木トランスデューサに関する理論であり，効率的かつ検証可能なソフトウェアへの応用が期待されている．本研究期間ではいくつかの木トランスデューサのクラス間の関係について研究を進めたが，特筆すべき結果として，効率のよいとされるストリーム型木トランスデューサのクラスが，等価性判定問題が決定可能である最大のクラスと一致することを示すことに成功した．この研究成果により，ある種の効率的なプログラムの検証アルゴリズムの開発が期待される．

  5. 確率的グラフィカルモデルの形式検証とその人工知能への応用

    Affeldt Reynald, 勝股 審也, 中野 圭介, J Garrigue

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

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

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

    研究機関：National Institute of Advanced Industrial Science and Technology

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

    詳細を見る 詳細を閉じる

    本研究では、確率とグラフを形式的に扱うように理論とツールを開発し、その応用実験も行った。定理証明支援系Coqを用いて、確率論及びより一般的なルベーグ積分の形式化を行った。木構造とグラフ構造に関する理論を開発し、そのデータ構造に基づくアルゴリズムの形式検証に応用した。以上の形式化を用いて、情報理論と人工知能の基礎の形式化を取り組んだ。確率的プログラムの形式検証のため、理論を開発し、定理証明支援系Coqを用いて確率を含むエフェクトを有するプログラムの形式検証基盤を開発した。本研究の成果の普及活動として、オープンソースソフトウェアを公開した。

  6. 定理証明支援系による形式木言語理論の定式化

    中野 圭介

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

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

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

    研究機関：The University of Electro-Communications

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

    詳細を見る 詳細を閉じる

    木構造データから木構造データへ変換するモデルである木トランスデューサ理論は，プログラミング言語理論やデータベース理論において重要な役割を果たしており，1960年代から盛んに研究が行われている．本研究の目的は，この理論を計算機の上で定式化し，その中の定理に対して機械的に検査可能な形の厳密な証明を与えることである．この成果により，今後の同分野の着実な発展が期待され，さらに堅牢なソフトウェア開発への応用の基盤を提供することが可能となる．

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

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

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

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

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

    研究機関：National Institute of Informatics

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

    詳細を見る 詳細を閉じる

    本研究は、大規模な実用に耐えうる双方向グラフ変換のための双方向変換言語の実現を目指して、まず、双方向変換の本質が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 (B)

    研究機関：National Institute of Informatics

    2010年4月1日 ～ 2014年3月31日

    詳細を見る 詳細を閉じる

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

  9. 実用的ウェブアプリケーション開発を支援するサーバサイドＪａｖａＳｃｒｉｐｔ処理系

    岩崎 英哉, 中野 圭介, 鵜川 始陽

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

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

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

    研究機関：The University of Electro-Communications

    2011年 ～ 2013年

    詳細を見る 詳細を閉じる

    本研究は，サーバ側で実用的な性能で動作する サーバサイドJavaScript処理系を開発することにより，煩雑な Web アプリケーション開発のコストを大きく低減させることを目指し，以下の成果を得た．(1) プログラムの実行情報を利用した最適化を行い実行速度を向上させるJavaScript処理系を構築した．(2) JavaScriptプログラムとC言語で記述されたプログラムとの連携を可能とする機構を構築した．(3) イベント駆動方式サーバのための並列JavaScript処理系を設計し実装した．(4) JavaScriptプログラムの安全な実行の基礎となる型システムを構築した．

  10. 木トランスデューサに基づく実用的な構造化文書変換の効率化と高信頼化

    中野 圭介

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

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

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

    研究機関：The University of Electro-Communications

    2010年 ～ 2012年

    詳細を見る 詳細を閉じる

    本研究課題の目標は,木トランスデューサ(TT)の理論をXML文書などの構造化文書の変換に応用し,TT理論の実用的側面を検証することである.TT理論は形式言語理論の研究者らが中心となり数学的興味から研究が進められてきたため,その実用性は疑問視されていたが,本研究の成果により構造化文書などの木構造データやその一般化であるグラフ構造データの変換プログラムの効率化や高信頼化に十分有用であることが確認できた.

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

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

  1. 情報論理学　東北大学

  2. アルゴリズム入門　University of Tokyo

  3. アルゴリズム入門　東京大学

  4. 情報科学　University of Tokyo

  5. 情報科学　東京大学

  6. プログラミング通論　電気通信大学

  7. ソフトウェア基礎特論　電気通信大学

  8. 情報工学演習第一　電気通信大学

  9. 情報工学実験第二　電気通信大学

  10. Computer Algorithms　電気通信大学

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