TOHOKU UNIVERSITY Researchers

Details of the Researcher

Home

日本語 English

Keisuke Nakano

Section

Research Institute of Electrical Communication

Job title

Professor

Degree

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

researchmap

https://researchmap.jp/-ksk

J-GLOBAL ID

200901023918073432

Research History 5

2018/04 - Present

Tohoku University　Research Institute of Electrical Communication　Professor
2013/06 - 2018/03

University of Electro-Communications　Faculty of Informatics and Engineering　Associate professor
2012/04 - 2013/05

The Education and Research Center for Frontier Science, The University of Electro-Communications　Associate professor
2008/03/01 - 2012/03/31

The Education and Research Center for Frontier Science, The University of Electro-Communications　Assistant Professor
2003/06/01 - 2008/02/29

Graduate School of Information Science and Technology, University of Tokyo　Researcher

Education 4

Kyoto University　Graduate School of Science　Research Institute for Mathematical Sciences

2000/04 - 2003/05
Kyoto University　Graduate School of Science　Research Institute for Mathematical Sciences

1997/04 - 2000/03
The University of Tokyo　Faculty of Science　Department of Mathematics

1996/04 - 1997/03
The University of Tokyo　College of Arts and Sciences

1994/04 - 1996/03

Committee Memberships 10

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

2022/04 - 2024/03
情報処理学会プログラミング研究会　主査

2020/04 - 2022/03
情報処理学会プログラミング研究会　幹事

2022/04 - Present
日本ソフトウェア科学会　編集委員

2013/04 - Present
情報処理学会プログラミング研究会　幹事

2017/04 - 2020/03
情報処理学会　会員サービス部門編集委員

2015/04 - 2019/03
情報処理学会　プログラミング研究会運営委員

2013/04 - 2017/03
日本ソフトウェア科学会　企画委員

2012/04 - 2016/03
日本ソフトウェア科学会　プログラミング論研究会運営委員

2012/04 - 2016/03
情報処理学会　プログラミング研究会論文誌編集委員

2009/04 - 2013/03

Show all ︎Show first 5

Professional Memberships 4

Institute of Electrical and Electronics Engineers (IEEE)

2019/01 - Present
日本ソフトウェア科学会
情報処理学会
Association for Computing Machinery (ACM)

Research Interests 7

Proof Assistants
Programming Language Theory
Formal Language Theory
Program Transformation
Bidirectional Transformation
Functional Programming
Tree Transducer Theory

Research Areas 2

Informatics / Software /
Informatics / Information theory /

Awards 4

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

2018/01　山内記念会　OCaml@p: OCaml におけるデバッグ出力機構
プログラミングシンポジウム山内奨励賞

2014/01　山内記念会　ジグソーパズルによる関数型プログラミング
ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation: A Best Paper Award

2012/01　Programming committee of ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation　Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals
第20回日本ソフトウェア科学会記念大会高橋奨励賞

2004/06　日本ソフトウェア科学会　Towards Implementation of XML Transformation Languages Intended for Stream Processing

Papers 79

Characterizations of Partial Well-Behaved Lenses. Peer-reviewed

Keishi Hashiba, Keisuke Nakano, Kazuyuki Asada, Kentaro Kikuchi

PEPM　43-53　2025

DOI： 10.1145/3704253.3706139 　
Lens Laws Zoo Invited Peer-reviewed

Keisuke Nakano

Bidirectional Collaborative Data Management　1　(1)　37-59　2024/12/12
Publisher: Springer Nature Singapore
DOI： 10.1007/978-981-97-6429-7_3 　
Disproving Termination of Non-erasing Sole Combinatory Calculus with Tree Automata International-journal Peer-reviewed

Keisuke Nakano, Munehiro Iwami

Lecture Notes in Computer Science　261-275　2024/09/03
Publisher: Springer Nature Switzerland
DOI： 10.1007/978-3-031-71112-1_19 　

ISSN： 0302-9743

eISSN： 1611-3349
Deciding Linear Height and Linear Size-To-Height Increase of Macro Tree Transducers Peer-reviewed

Paul Gallot, Sebastian Maneth, Keisuke Nakano, Charles Peyrat

51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)　138:1-138:20　2024/07

DOI： 10.4230/LIPIcs.ICALP.2024.138 　
Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)

Keisuke Nakano, Munehiro Iwami

2024/06/20

DOI： 10.48550/arXiv.2406.14305 　
Deciding Linear Height and Linear Size-to-Height Increase for Macro Tree Transducers

Paul Gallot, Sebastian Maneth, Keisuke Nakano, Charles Peyrat

2023/07/31

DOI： 10.48550/arXiv.2307.16500 　
Time-symmetric Turing machines for computable involutions Peer-reviewed

Keisuke Nakano

Science of Computer Programming　215　102748-102748　2022/03
Publisher: Elsevier BV
DOI： 10.1016/j.scico.2021.102748 　

ISSN： 0167-6423
Bidirectional Collaborative Frameworks for Decentralized Data Management Invited Peer-reviewed

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
Publisher: Springer International Publishing
DOI： 10.1007/978-3-030-93849-9_2 　

ISSN： 1865-0929

eISSN： 1865-0937
A Tangled Web of 12 Lens Laws. Peer-reviewed

Keisuke Nakano

13th International Conference on Reversible Computation (RC)　185-203　2021
Publisher: Springer
DOI： 10.1007/978-3-030-79837-6_11 　
Idempotent Turing Machines Peer-reviewed

Keisuke Nakano

46th International Symposium on Mathematical Foundations of Computer Science (MFCS)　79:1-79:18　2021
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
DOI： 10.4230/LIPIcs.MFCS.2021.79 　
Streaming ranked-tree-to-string transducers. Peer-reviewed

Yuta Takahashi, Kazuyuki Asada, Keisuke Nakano

Theoretical Computer Science　870　165-187　2021

DOI： 10.1016/j.tcs.2020.12.033 　
On properties of B-terms Peer-reviewed

Mirai Ikebuchi, Keisuke Nakano

Logical Methods in Computer Science　16　(2)　2020/06
Involutory Turing Machines Peer-reviewed

Keisuke Nakano

Reversible Computation　12227　54-70　2020
Publisher: Springer International Publishing
DOI： 10.1007/978-3-030-52482-1_3 　

ISSN： 0302-9743

eISSN： 1611-3349
Towards a Complete Picture of Lens Laws Peer-reviewed

Keisuke Nakano

3rd Workshop on Software Foundations for Data Interoperability (SFDI2019+)　2019/10
Streaming Ranked-Tree-to-String Transducers International-journal Peer-reviewed

Yuta Takahashi, Kazuyuki Asada, Keisuke Nakano

24th International Conference on Implementation and Application of Automata, CIAA 2019　11601　235-247　2019/07
Publisher: Springer
DOI： 10.1007/978-3-030-23679-3_19 　
Toward BX-Based Architecture for Controlling and Sharing Distributed Data Peer-reviewed

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

IEEE Second Workshop on Software Foundations for Data Interoperability (SFDI 2019)　2019/02
Flexible Framework for Data Integration and Update Propagation: System Aspect Peer-reviewed

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/02
Publisher: IEEE
DOI： 10.1109/BIGCOMP.2019.8679236 　
On Repetitive Right Application of B-Terms. International-coauthorship Peer-reviewed

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/07
Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
DOI： 10.4230/LIPIcs.FSCD.2018.18 　
Making View Update Strategies Programmable - Toward Controlling and Sharing Distributed Data -. Peer-reviewed

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
A View-based Programmable Architecture for Controlling and Integrating Decentralized Data. Peer-reviewed

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
Towards practical typechecking for macro forest transducers Peer-reviewed

Kazuhiro Abe, Keisuke Nakano

Journal of Information Processing　25　962-974　2017/12/01
Publisher: Information Processing Society of Japan
DOI： 10.2197/ipsjjip.25.962 　

ISSN： 1882-6652 0387-5806
Bidirectional Certified Programming. Peer-reviewed

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/04
Publisher: CEUR-WS.org
マクロ森トランスデューサの実用的な型検査に向けて

阿部和敬, 中野圭介

第113回プログラミング研究発表会　2017/03
属性文法合成による関数融合の実装 Peer-reviewed

中川涼太, 中野圭介

第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) 予稿集　2017/03
木から文字列への決定性トップダウン変換の等価性判定の実装 Peer-reviewed

高橋祐多, 中野圭介

第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017) 予稿集　2017/03
On repetitive right application of B-terms.

Mirai Ikebuchi, Keisuke Nakano

CoRR　abs/1703.10938　2017/03
既存のコード資産を利用した制御構文補完機構

北原元気, 中野圭介

第58回プログラミング・シンポジウム予稿集　2017/01
Context-preserving XQuery fusion Peer-reviewed

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

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE　25　(4)　916-941　2015/05

DOI： 10.1017/S096012951300008X 　

ISSN： 0960-1295

eISSN： 1469-8072
Grammatical Frameworkにおける語彙データの自動生成

渡邉秀隆, 中野圭介

言語処理学会第21回年次大会論文集　836-839　2015/03
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
XQuery Streaming by Forest Transducers Peer-reviewed

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
Structural Recursion for Querying Ordered Graphs Peer-reviewed

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

ACM SIGPLAN NOTICES　48　(9)　305-318　2013/09

DOI： 10.1145/2500365.2500608 　

ISSN： 0362-1340

eISSN： 1558-1160
Structural Recursion for Querying Ordered Graphs Peer-reviewed

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

第15回プログラミングおよびプログラミング言語ワークショップ (PPL2013) 予稿集　2013/03
JavaScript 仮想機械におけるQuickeningの効果 Peer-reviewed

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

第15回プログラミングおよびプログラミング言語ワークショップ (PPL2013) 予稿集　2013/03
Metamorphism in jigsaw Peer-reviewed

Keisuke Nakano

Journal of Functional Programming　23　(2)　161-173　2013/03

DOI： 10.1017/S0956796812000391 　

ISSN： 0956-7968 1469-7653
GRoundTram: An integrated framework for developing well-behaved bidirectional model transformations Peer-reviewed

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

Progress in Informatics　10　(10)　131-148　2013/03

DOI： 10.2201/NiiPi.2013.10.7 　

ISSN： 1349-8614 1349-8606
ジグソーパズルによる関数型プログラミング

中野圭介

第54回プログラミング・シンポジウム予稿集　2013/01
A parameterized graph transformation calculus for finite graphs with monadic branches Peer-reviewed

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 　
Optimization for iterative queries on MapReduce Peer-reviewed

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

Proceedings of the VLDB Endowment　7　(4)　241-252　2013
Publisher: Association for Computing Machinery
DOI： 10.14778/2732240.2732243 　

ISSN： 2150-8097
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
View Updatability Checking with Simulation-based Graph Schema Peer-reviewed

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

Computer Software　29　(2)　174-192　2012/05

DOI： 10.11309/jssst.29.2_174 　
Polynomial-time inverse computation for accumulative functions with multiple data traversals Peer-reviewed

Kazutaka Matsuda, Kazuhiro Inaba, Keisuke Nakano

Higher-Order and Symbolic Computation　25　(1)　3-38　2012/03/01
Publisher: Kluwer Academic Publishers
DOI： 10.1007/s10990-013-9097-8 　

ISSN： 1388-3690
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
Publisher: Association for Computing Machinery
DOI： 10.1145/2103746.2103752 　

ISSN： 0730-8566
Context-Preserving XQuery Fusion Peer-reviewed

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

Mathematical Structures in Computer Science (MSCS), Cambridge University Press　916-941　2012
Marker-directed optimization of UnCAL graph transformations Peer-reviewed

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
Shall we juggle, coinductively? Peer-reviewed

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
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
漸進的グラフビュー維持の枠組みの提案

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

日本ソフトウェア科学会第28 回大会講演論文集　2011/09
模倣に基づくグラフスキーマを利用したビュー更新可能性判定 Peer-reviewed

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

第13回プログラミングおよびプログラミング言語ワークショップ論文集　146-160　2011/03
GRoundTram: An integrated framework for developing well-behaved bidirectional model transformations Peer-reviewed

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 　
Toward bidirectionalization of ATL with GRoundTram Peer-reviewed

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
Graph-Transformation Verification using Monadic Second-Order Logic Peer-reviewed

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 　
Bidirectionalizing Graph Transformations Peer-reviewed

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

ACM SIGPLAN NOTICES　45　(9)　205-216　2010/09

DOI： 10.1145/1932681.1863573 　

ISSN： 0362-1340

eISSN： 1558-1160
Bidirectionalizing Graph Transformations Peer-reviewed

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

ICFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING　205-216　2010
Context-preserving XQuery fusion Peer-reviewed

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
順序を考慮にいれたXQueryの融合変換 Peer-reviewed

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

Webとデータベースに関するフォーラム(WebDB Forum 2009)　2009/11
Bidirectionalizing Structural Recursion on Graphs

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

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

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

日本ソフトウェア科学会第26回大会 , 島根大学（松江キャンパス）, 2009年9月16日(水)～18日(金)　2009/09
Bidirectionalizing programs with Duplication through Complementary Function Derivation Peer-reviewed

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

Computer Software　26　(2)　56-75　2009/06
Publisher: Japan Society for Software Science and Technology
DOI： 10.11309/jssst.26.2_56 　

ISSN： 0289-6540

More details Close

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

Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

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

DOI： 10.1145/1529282.1529383 　
Rewriting XQuery to Avoid Redundant Expressions based on Static Emulation of XML Store Peer-reviewed

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/01
A Compositional Approach to Bidirectional Model Transformation Peer-reviewed

Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

2009 31ST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, COMPANION VOLUME　235-+　2009

DOI： 10.1109/ICSE-COMPANION.2009.5070990 　

ISSN： 0270-5257
Composing Stack-Attributed Tree Transducers Peer-reviewed

Keisuke Nakano

THEORY OF COMPUTING SYSTEMS　44　(1)　1-38　2009/01

DOI： 10.1007/s00224-008-9125-y 　

ISSN： 1432-4350

eISSN： 1433-0490
Computing the Cost of Typechecking of Composition of Macro Tree Transducers Peer-reviewed

Keisuke Nakano, Sebastian Maneth

Information and Media Technologies　4　(4)　846-856　2009
Publisher: Information and Media Technologies Editorial Board
DOI： 10.11185/imt.4.846 　

More details Close

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.
Consistent Web site updating based on bidirectional transformation Peer-reviewed

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
Development of Bidirectional XML Applications Using Dependency Description Schema

HAYASHI Yasushi, LIU Dongxi, NAKANO Keisuke, HU Zhenjiang, TAKEICHI Masato

70　(5)　"5-393"-"5-394"　2008/03/13
Publisher:
Vu-X : Web Publishing System based on Bidirectional Transformation

NAKANO Keisuke, LIU Dongxi, HAYASHI Yasushi, HU Zhenjiang, TAKEICHI Masato

70　(5)　"5-391"-"5-392"　2008/03/13
Publisher:
補関数の生成による複製を含むプログラムの自動双方向化

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

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

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

情報処理学会第70回全国大会, 筑波大学筑波キャンパス, 平成20年3月13日(木)〜15日(土).　2008/03
Consistent web site updating based on bidirectional transformation Peer-reviewed

Keisuke Nakano, Zhenjiang Hu, Masato Takeichi

Proceedings - 10th IEEE International Symposium on Web Site Evolution, WSE 2008　45-54　2008
Publisher: IEEE Computer Society
DOI： 10.1109/WSE.2008.4655395 　
Bidirectionalization transformation based on automatic derivation of view complement functions Peer-reviewed

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

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

ISSN： 0362-1340
対話的データ操作による双方向変換プログラミング

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

日本ソフトウェア科学会第24回大会 , 奈良先端科学技術大学院大学, 2007年9月12日(水)〜14日(金)　2007/09
Bidirectionalization Transformation Based on Automatic Derivation of View Complement Functions Peer-reviewed

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

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

DOI： 10.1145/1291151.1291162 　

ISSN： 0362-1340
XML stream transformer generation through program composition and dependency analysis Peer-reviewed

S Nishimura, K Nakano

SCIENCE OF COMPUTER PROGRAMMING　54　(2-3)　257-290　2005/02

DOI： 10.1016/j.scico.2004.07.001 　

ISSN： 0167-6423

eISSN： 1872-7964
By-Need Evaluation of Programmable Structured Documents

Nishioka Shingo, Nakano Keisuke, Hu Zhenjiang, Takeichi Masato

Conference Proceedings of Japan Society for Software Science and Technology　21　42-42　2004/09
Publisher: Japan Society for Software Science and Technology
DOI： 10.11309/jssstconference.21.0.42.0 　

ISSN： 1349-3515

More details Close

PSD (Programmable Structured Documents) is a safe document processing framework for structured documents, such as XML. In the PSD framework, a document is processed by an external processor which is an independent process other than the document holding process. Therefore, we need an effective mechanism to pass the evaluated document between the processes. By-Need DOM provides a remote access method to an embedded DOM data on another process. By-Need DOM transfers the required part of documents, when the data becomes really needed by the evaluator, minimizing the total amount of transfered data. The part of documents is specified by XPath notation. Furthermore, By-Need DOM implements the minimal methods required by the PSD evaluator. This makes the code simple and highly portable.
Towards Implementation of XML Transformation Languages Intended for Stream Processing. Peer-reviewed

Keisuke Nakano

Computer Software　21　(3)　206-212　2004

DOI： 10.11309/jssst.21.206 　

ISSN： 0289-6540
TreeCalc : Towards Programmable Structured Documents

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

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

DOI： 10.11309/jssstconference.2003.0.81.0 　

ISSN： 1349-3515

More details Close

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.
Automatic Deriviation of Event-Based Document Transformations. Peer-reviewed

Keisuke Nakano, Susumu Nishimura

Computer Software　19　(4)　289-295　2002

DOI： 10.11309/jssst.19.289 　

ISSN： 0289-6540
Deriving event-based document transformers from tree-based specifications Peer-reviewed

Keisuke Nakano, Susumu Nishimura

Electronic Notes in Theoretical Computer Science　44　(2)　187-211　2001/06

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

ISSN： 1571-0661

Show all ︎Show first 5

Misc. 25

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

櫻井健二, 中野圭介

第58回プログラミング・シンポジウム予稿集　2017/01
Rubyに対するGradual typingの導入に向けて

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

第58回プログラミング・シンポジウム予稿集　2017/01
Ruby on Railsにおけるテストケース自動生成の提案と実装'

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

第93回プログラミング研究発表会　2013/03
JavaScriptにおけるプログラム変換の効果

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

情報処理学会夏のプログラミング・シンポジウム報告集　2011　19-26　2012/01/06
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/05
GRoundTramによるATLの双方向化の実現

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

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

ISSN： 1348-0901
漸進的グラフビュー更新の枠組みの提案

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

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

ISSN： 1348-0901
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
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
Complete Validation of Graph Transformations

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

GRACE Technical Report GRACE-TR-2010-04　2010/05
順序を考慮に入れたXQueryの融合変換

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

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

ISSN： 1882-0840
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/09

ISSN： 1884-0760
Computing the Cost of Typechecking of Composition of Macro Tree Transducers

Keisuke Nakano, Sebastian Maneth

2　(4)　53-63　2009/08/28
Publisher: 情報処理学会
ISSN： 1882-7802
An Algebraic Approach to Bidirectional Model Transformations

Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

Technical Report GRACE-TR-2008-02　2008/09
Towards Compositional Approach to Model Transformations

Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

Technical Report GRACE-TR-2008-01　2008/08
Bidirectional XML Transformation with Bi-X

LIU Dongxi, HAYASHI Yasushi, NAKANO Keisuke, HU Zhenjiang, TAKEICHI Masato

70　(5)　"5-395"-"5-396"　2008/03/13
Publisher: 社団法人情報処理学会
依存関係記述スキーマによる双方向XMLアプリケーションの開発

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

情報処理学会全国大会講演論文集　70th　(5)　5.393-5.394　2008/03/13
双方向変換に基づくウェブパブリッシング支援システムVu‐X

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

情報処理学会全国大会講演論文集　70th　(5)　5.391-5.392-392　2008/03/13
構造化文書の依存関係記述のための拡張スキーマ

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

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

ISSN： 1348-0901
双方向変換に基づくウェブページ更新機構

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

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

ISSN： 1348-0901
Macro Forest TransducerからのXMLストリーム処理器の自動導出

中野圭介

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

ISSN： 1348-0901
構造化文書の応需計算機構

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

日本ソフトウエア科学会大会講演論文集(CD-ROM)　21st　3D-3-42　2004
Publisher: Japan Society for Software Science and Technology
DOI： 10.11309/jssstconference.21.0.42.0 　

ISSN： 1348-0901

More details Close

PSD (Programmable Structured Documents) is a safe document processing framework for structured documents, such as XML. In the PSD framework, a document is processed by an external processor which is an independent process other than the document holding process. Therefore, we need an effective mechanism to pass the evaluated document between the processes. By-Need DOM provides a remote access method to an embedded DOM data on another process. By-Need DOM transfers the required part of documents, when the data becomes really needed by the evaluator, minimizing the total amount of transfered data. The part of documents is specified by XPath notation. Furthermore, By-Need DOM implements the minimal methods required by the PSD evaluator. This makes the code simple and highly portable.
XMLストリーム処理器の自動導出が可能なXML変換言語の設計

中野圭介

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

ISSN： 0913-5391
SOBAに基づいた共著支援システム

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

情報処理学会全国大会講演論文集　65th　(4)　4.1-4.2　2003/03/25
イベント駆動型文書変換器の自動生成

中野圭介, 西村進

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

ISSN： 0913-5391

Show all ︎Show first 5

Books and Other Publications 1

The Little Prover

Daniel Friedman, Carl Eastlund, Keisuke NAKANO

2017/10

ISBN: 9784908686023

Presentations 3

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

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

第14回プログラミングおよびプログラミング言語ワークショップ（PPL2012）　2012/03
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
模倣に基づくグラフスキーマを利用したビュー更新可能性判定

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

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

Research Projects 10

Formal Foundations for Verification of Physical and Probabilistic Systems

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research

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

Institution: National Institute of Advanced Industrial Science and Technology

2022/04/01 - 2026/03/31
双方向変換言語のための計算モデルとプログラミング言語への応用

中野圭介

Offer Organization: 日本学術振興会

System: 科学研究費助成事業

Category: 基盤研究(C)

Institution: 東北大学

2021/04/01 - 2025/03/31

More details Close

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

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

Offer Organization: 日本学術振興会

System: 科学研究費助成事業

Category: 基盤研究(A)

Institution: 京都大学

2018/04/01 - 2022/03/31

More details Close

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

Nakano Keisuke

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research

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

2017/04/01 - 2022/03/31

More details Close

Formal tree language theory is a theory of tree automata and tree transducers for a formal model of tree-structured data, and is expected to be applied to efficient and verifiable software. In this research project, we have studied the relation between several classes of tree transducers and succeeded in showing that the class of stream-type tree transducers that is considered efficient corresponds to the largest class in which the equivalence problem is decidable. The results of this research are expected to lead to the development of some efficient program verification algorithms.
Formal verification of probabilistic graphical models and its application to artificial intelligence

Affeldt Reynald

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research

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

Institution: National Institute of Advanced Industrial Science and Technology

2018/04/01 - 2021/03/31

More details Close

In this project we develop several formal tools to deal formally with probability and graphs. We provide a formalization of probability theory and more generally of Lebesgue integration in the Coq proof assistant. We develop theories to reason about tree and graph structures and apply them to the formal verification of programs. We applied the resulting theories to the formalization of the bases of information theory and artificial intelligence. We also develop theories to verify probabilistic programs and provide a generic and extensible framework to verify effectful programs in the Coq proof assistant. Most of our results are available as open access papers and open source software.
Mechanized formalization of formal tree languages in proof assistants

Keisuke Nakano

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research

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

Institution: The University of Electro-Communications

2013/04/01 - 2017/03/31

More details Close

The theory of tree transducers which models tree-to-tree transformations has been explored since 1960's and played an important role in theory of programming languages and databases. The goal of this project is to formalize the theory in computer where all proofs of theorems for tree transducers are mechanically ceritified. It enables us to easily and steadily expand the theory and apply it to development of robust softwares.
Integrated and Fundamental for Large-Scale and Practical Bidirectional Graph Transformation

Hu Zhenjiang, EMOTO Kento, MORIHATA Akimasa, MATSUDA Kazutaka, ZHU Zirun

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research

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

Institution: National Institute of Informatics

2013/04/01 - 2017/03/31

More details Close

In this research, to realize a bidirectional transformation language that can be used to deal with large scale graphs in practice, we provided a new foundation for bidirectional transformation, showing that the essence of bidirectional transformation is "putback" transformation. Based on this foundation, we succeeded in designing and implementing a new bidirectional transformation language BiGUL, which cannot only fully describe the behavior of bidirectional transformation but also guarantee the roundtrip property. Also, we extended our previous bidirectional graph transformation mechanism so that it can deal with various graph structures, and applied to bidirectionalize model transformations in ATL, a language widely used in model driven software development. Finally, we evaluated the usefulness of our approach by developing several useful systems, including the BiYacc system for supporting development of bidirectional transformations between source programs and abstract syntax trees.
Study on Language Foundation for Bidirectional Model Transformation

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

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research

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

Institution: National Institute of Informatics

2010/04/01 - 2014/03/31

More details Close

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

IWASAKI Hideya, NAKANO Keisuke, UGAWA Tomoharu

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research

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

Institution: The University of Electro-Communications

2011 - 2013

More details Close

This research aims to develop an efficient server-side JavaScript engine that is expected to reduce the development cost of web applications. The obtained results can be summarized as follows. (1) We have developed a JavaScript virtual machine that optimizes the program execution on the basis of run-time information. (2) We have developed a foreign function interface that enables the programmer to call C functions from a JavaScript program. (3) We have extended the JavaScript virtual machine described in (1) so that it can run in parallel as event-driven servers. (4) We have developed a gradual type system for a subset of JavaScript programs to be a base of their safe execution.
Efficient implementation and verification of practical structured-document transformation based on tree transducer theory

NAKANO Keisuke

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research

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

Institution: The University of Electro-Communications

2010 - 2012

More details Close

The goal of this research project is to demonstrate the practicality of the theory of tree transducers (TTs) by applying it to transformation of structured documents such as the XML format. The TT theory has been intensively studied by researchers in formal language theory from the mathematical point of view. The project representative confirmed the practicality of TT streaming and TT verification by extending existing results on composition and typechecking TTs.

Show all Show first 5

Teaching Experience 10

情報論理学　東北大学
アルゴリズム入門　University of Tokyo
アルゴリズム入門　東京大学
情報科学　University of Tokyo
情報科学　東京大学
プログラミング通論　電気通信大学
ソフトウェア基礎特論　電気通信大学
情報工学演習第一　電気通信大学
情報工学実験第二　電気通信大学
Computer Algorithms　電気通信大学

Show all Show first 5