東北大学 電気通信研究所

研究室外部評価 参考資料
(2013 年度-2018 年度)

Research Laboratory Reference Datafor External Review
April 2013 - March 2019
(FY.2013-2018)

Research Institute of Electrical Communication
Tohoku University

ソフトウェア構成研究室

Software Construction

1 研究成果 / Research Activities
Notation for Japanese publications.
• The items with the “(in Japanese)” annotation are those Japanese publications that carry
English titles in the original articles.
• The items with the “(translation: )” annotation are those that do not carry English titles.

(1) 査読付学術論文 / Refereed Journal Papers[1-1] Masanori Endo, Yuto Mukade, Akimasa Morihata, Katsuhiro Ueno, Atsushi Ohori: Code Reading Assistance for Functional Programming based on Variable Def-use Relationships. Computer
Software, Vol.32, No.1, pp.1 194-1 212, February, 2015. (in Japanese)[1-2] Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: Automated Inductive Theorem Proving using Transformations of Term Rewriting Systems. Computer Software, Vol.32,
No.1, pp.1 179-1 193, 2015. (in Japanese)[1-3] Katsuhiro Ueno, Atsushi Ohori, and Toshiaki Otomo.
An Eﬃcient Non-Moving Garbage Collector for Functional Languages,
Higher-Order and Symbolic Computation, Springer,
40 pages, accepted for publication on Dec. 17th, 2015.
[1-4] Katsuhiro Ueno, Atsushi Ohori: A Type Safe Access to Key-value Stores from Functional
Languages, Journal of Information Processing, Vol. 24(2016), No. 1, pp.141-151, Jan. 2016
[1-5] Katsuhiro Ueno, Atsushi Ohori. A foreign language interface from ML to shell. New Generation
Computing, Vol. 34, No. 3, pp. 239–256, 2016．
[1-6] Mifuyu Osaka, Katsuhiro Ueno, Atsushi Ohori: Typed template engine based on partiallydynamic records. Computer Software, Vol.35, No.3, pp.3 79-3 95, July, 2018. (in Japanese)[1-7] Kazuki Ono, Katsuhiro Ueno, Atsushi Ohori: Implementation Method of Native Code Level
Debugging Environment for SML#. IPSJ Transactions on Programming (PRO), Vol.11, No.3,
pp.1-13, September, 2018. (in Japanese)(2) 原著論文と同等に扱う査読付き国際会議発表論文
Full papers in refereed conference proceedings equivalent to journal papers[1-8] Kentaro Kikuchi: Proving Strong Normalization via Non-deterministic Translations into Klop’s
Extended λ-Calculus, Proceedings of the 22nd Annual Conference of the European Association
for Computer Science Logic (CSL 2013), LIPIcs 23, pp.395-414, September, 2013.
[1-9] Atsushi Ohori, Katsuhiro Ueno, Kazunori Hoshi, Shinji Nozaki, Takashi Sato, Tasuku Makabe,
Yuki Ito. SML# in Industry: A Practical ERP System Development. Proceedings of the ACM
International Conference on Functional Programming (ICFP), pages 167 - 173, 2014.
[1-10] Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: Confluence of Orthogonal
Nominal Rewriting Systems Revisited, Proceedings of the 26th International Conference on
Rewriting Techniques and Applications (RTA 2015), LIPIcs 36, pp.301-317, 2015.
[1-11] Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: Correctness of ContextMoving Transformations for Term Rewriting Systems, Proceedings of the 25th International

2Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015), LNCS
9527, pp.331-345, 2015.
[1-12] Atsushi Ohori, Katsuhiro Ueno, Tomohiro Sasaki, Daisuke Kikuchi. A Calculus with Partially
Dynamic Records for Typeful Manipulation of JSON Objects．Proceedings of the 30th European Conference on Object-Oriented Programming (ECOOP 2016), pp. 18:1–18:25, 2016．
[1-13] Katsuhiro Ueno, Atsushi Ohori. A fully concurrent garbage collector for functional programson multicore processors. Proceedings of the 21st ACM SIGPLAN International Conference on
Functional Programming (ICFP 2016), pp. 421–433. 2016．
[1-14] Atsushi Ohori, Katsuhiro Ueno, Hisayuki Mima: Finitary Polymorphism for Optimizing TypeDirected Compilation, In Proceedings of the 23rd Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’18), St. Louis, 2018.

(3) 査読付国際会議 / Papers in refereed conference proceedings[1-15] Atsushi Ohori: Record Polymorphism: Its Development and Applications, In Search of Elegancein the Theory and Practice of Computation, Lecture Notes in Computer Science, Volume 8000,
pp 432-444, University of Edinburgh, Oct. 28th, 2013.
[1-16] Akimasa Morihata, Masato Koishi, Atsushi Ohori Dynamic Programming via Thinning andIncrementalization. Proceedings of the International Symposium on Functional and Logic Programming (FLOPS), pages 186 - 202, June 2014.
[1-17] Kentaro Kikuchi, Takafumi Sakurai: A Translation of Intersection and Union Types for the λμ-Calculus (short paper), Proceedings of the 5th International Workshop on Classical Logic
and Computation (CL&C 2014), 2014.
[1-18] Katsuhiro Ueno, Atsushi Ohori. Compiling SML# with LLVM: a Challenge of Implementing
ML on a Common Compiler Infrastructure. ACM SIGPLAN ML Family Workshop 2014.
[1-19] Kentaro Kikuchi, Takafumi Sakurai: A Translation of Intersection and Union Types for the λμCalculus, Proceedings of the 12th Asian Symposium on Programming Languages and Systems(APLAS 2014), LNCS 8858, pp.120-139, 2014.
[1-20] Katsuhiro Ueno, Atsushi Ohori: A foreign language interface from ML to shell. Symposium on
Trends in Functional Programming 2014 (TFP 2014), 2014.
[1-21] Katsuhiro Ueno, Yutaka Fukasawa, Akimasa Morihata, Atsushi Ohori. The Essence of Ruby.
Asian Symposium on Programming Languages and Systems (APLAS), pages 78 - 98, Nov. 2014.
[1-22] Kentaro Kikuchi: Uniform Proofs of Normalization and Approximation for Intersection Types,
Proceedings of the 7th Workshop on Intersection Types and Related Systems (ITRS 2014),
EPTCS 177, pp.10-23, 2015.
[1-23] Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: Context-Moving Transformation for Term Rewriting Systems (Extended Abstract), Participant’s Proceedings of the 2nd
International Workshop on Rewriting Techniques for Program Transformations and Evaluation(WPTE 2015), pp.3-7, 2015.
[1-24] Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: Critical Pair Analysis in
Nominal Rewriting, Proceedings of the 7th International Symposium on Symbolic Computation
in Software Science (SCSS 2016), EPiC 39, pp.156-168, 2016.
[1-25] Takahito Aoto, Kentaro Kikuchi: A Rule-Based Procedure for Equivariant Nominal Unification,
Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR 2016), 2016.
[1-26] Takahito Aoto, Kentaro Kikuchi: Nominal Confluence Tool, Proceedings of the 8th International3

Joint Conference on Automated Reasoning (IJCAR 2016), LNAI 9706, pp.173-182, 2016.
[1-27] Tomohiro Sasaki, Katsuhiro Ueno, Atsushi Ohori. SML# with Natural Join. ACM SIGPLAN
Workshop on ML, 2016.
[1-28] Kentaro Kikuchi: Confluence by Strong Commutation with Disjoint Parallel Reduction, Participant’s Proceedings of the 4th International Workshop on Rewriting Techniques for Program
Transformations and Evaluation (WPTE 2017), 2017.
[1-29] Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: Parallel Closure Theorem for Left-Linear
Nominal Rewriting Systems, Proceedings of the 11th International Symposium on Frontiers of
Combining Systems (FroCoS 2017), LNAI 10483, pp.115-131, 2017.
[1-30] Atsushi Ohori, Kenjiro Taura, Katsuhiro Ueno: Making SML# a general-purpose highperformance language. ACM SIGPLAN Workshop on ML, 2017.

(4) 査読なし国際会議・シンポジウム等 / Papers in unrefereed conference(5) 総説・解説 / Review articles[1-31] Atsushi Ohori: Principles of LR Parsing. Computer Software, Vol.31, No.1, pp.1 30-1 42, 2014.
(in Japanese)(6) 査読付国内会議 / Refereed domestic conferences[1-32] 斎藤皓, 上野雄大, 森畑明昌, 大堀淳. SML#の SQL 統合機能への行集約機能の実装. 第 16 回プロ
グラミングおよびプログラミング言語ワークショップ, 2014 年 3 月．(translation: Hikaru Saito,
Katsuhiro Ueno, Akimasa Morihata, Atsushi Ohori: Integration of the SQL row aggregation
feature into SML#, 16th JSSST Workshop on Programming and Programming Languages,
March, 2014. )[1-33] 佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人: 帰納的定理自動証明のための項書き換えシステム自動変換, 第 16 回プログラミングおよびプログラミング言語ワークショップ (PPL 2014), 2014 年 3 月 5 日.
(translation: Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: AutomatedTransformations of Term Rewriting Systems for Automated Inductive Theorem Proving. 16th
JSSST Workshop on Programming and Programming Languages, March, 2014. )[1-34] 鈴木貴樹, 菊池健太郎, 青戸等人, 外山芳人: 名目書き換えシステムの合流性について, 第 16 回プログ
ラミングおよびプログラミング言語ワークショップ (PPL 2014), 2014 年 3 月 5 日. (translation:
Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: On Confluence of Nominal
Rewriting Systems. 16th JSSST Workshop on Programming and Programming Languages,
March, 2014. )[1-35] 魚谷孝太, 上野雄大, 大堀淳: Java PathFinder?による ML プログラムの捕捉されない例外の検証（登壇発表＆ポスター発表）, The 2nd. cross-disciplinary Workshop on Computing Systems, Infrastructures, and Programming (xSIG 2018), 一橋講堂, 査読あり, 2018 年 5 月 29 日. (translation:
Kota Uotani, Katsuhiro Ueno, Atsushi Ohori: Verification of uncaught exceptions in ML by Java
PathFinder, The 2nd cross-disciplinary Workshop on Computing Systems, Infrastructures, andProgramming (xSIG 2018), May, 2018. )[1-36] 高城光平, 上野雄大, 大堀淳: ML 系言語とストリーミングデータベースの統合（登壇発表＆ポスター発表）, The 2nd. cross-disciplinary Workshop on Computing Systems, Infrastructures,
and Programming (xSIG 2018), 一橋講堂, 査読あり, 2018 年 5 月 29 日. (translation: Kohei

4Takagi, Katsuhiro Ueno, Atsushi Ohori: Integration of an ML-family language and streaming
database, The 2nd. cross-disciplinary Workshop on Computing Systems, Infrastructures, andProgramming (xSIG 2018), May, 2018. )[1-37] 遠藤侑介, 松本宗太郎, 上野雄大, 住井英二郎, 松本行弘: Progress report: Ruby 3 における静的型解
析の実現に向けて, 第 21 回プログラミングおよびプログラミング言語ワークショップ（PPL2019）,
湯の杜ホテル志戸平, 2019 年 3 月 6 日. (translation: Yusuke Endo, Soutaro Matsumoto,Katsuhiro Ueno, Eijiro Sumii, Yukihiro Matsumoto: Progress report: Toward static analysis
in Ruby 3 The 21st JSSST Workshop on Programming and Programming Languages, March,2019. )

(7) 査読なし国内研究会・講演会 / Unrefereed domestic conferences[1-38] 佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人: 自動検証のためのプログラム変換法, 日本ソフト
ウェア科学会第 30 回大会, 東京大学本郷キャンパス, 2013 年 9 月 10 日. (translation: Koichi
Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: Program Transformation for Automated Verification. Annual Meeting of the Japan Society for Software Science and Technology,
September, 2013. )[1-39] 上野雄大, 大堀淳. 関数型言語からキーバリューストアへの型安全なアクセス機構．日本ソフトウェ
ア科学会第 30 回大会，東京大学，2013 年 9 月 11 日．(translation: Katsuhiro Ueno, Atsushi
Ohori: Type-safe access from an functional language to a key-value store. Annual Meeting of
the Japan Society for Software Science and Technology, September, 2013. )[1-40] 遠藤誠典, 百足勇人, 森畑明昌, 上野雄大, 大堀淳. 変数参照関係を用いた関数型プログラムの
コードリーディング支援．日本ソフトウェア科学会第 30 回大会，東京大学，2013 年 9 月 11 日．
(translation: Masanori Endo, Yuto Mukade, Akimasa Morihata, Katsuhiro Ueno, Atsushi
Ohori: Assisting reading functional program code by def-use relationship of variables. Annual
Meeting of the Japan Society for Software Science and Technology, September, 2013. )[1-41] 日本ソフトウェア科学会 第 31 回大会 トップカンファレンス特別講演 Atsushi Ohori, Katsuhiro
Ueno, Kazunori Hoshi, Shinji Nozaki, Takashi Sato, Tasuku Makabe, Yuki Ito SML# in Industry: A Practical ERP System Development (ACM ICFP 2014 にて発表) 名古屋大学, 2014 年 9 月
10 日. (translation: Atsushi Ohori, Katsuhiro Ueno, Kazunori Hoshi, Shinji Nozaki, Takashi
Sato, Tasuku Makabe, Yuki Ito: SML# in Industry: A Practical ERP System Development(invited special lecture of a top-conference paper). Annual Meeting of the Japan Society for
Software Science and Technology, September, 2014. )[1-42] 逢坂美冬, 佐々木智啓, Charles Mejia Cruz, 上野雄大, 大堀淳. 関数型言語 SML#における 64
ビット対応への取り組み, 日本ソフトウェア科学会第 31 回大会, 名古屋大学，2014 年 9 月 10 日.
(translation: Mifuyu Osaka, Tomohiro Sasaki, Charles Mejia Cruz, Katsuhiro Ueno, Atsushi
Ohori: Progress report on 64-bit SML#. Annual Meeting of the Japan Society for Software
Science and Technology, September, 2014. )[1-43] 菊池健太郎, 青戸等人, 外山芳人: 文脈移動法によるプログラム変換の正当性について, 日本ソフトウェア科学会第 32 回大会, 早稲田大学西早稲田キャンパス, 2015 年 9 月 8 日. (translation:
Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama: On the Correctness of Context-Moving
Transformations. Annual Meeting of the Japan Society for Software Science and Technology,
September, 2015. )[1-44] 上野雄大, 大堀淳: 関数型言語からキーバリューストアへの型安全なアクセス機構, 富山県教育文化会
館, 情報処理学会 第 104 回プログラミング研究発表会, 2015 年 6 月 5 日. (translation: Katsuhiro
5

Ueno, Atsushi Ohori: A Type Safe Access to Key-value Stores from Functional Languages.
The 104th meeting of Special Interest Group on Programming (PRO), Information Processing
Society of Japan, June, 2015. )[1-45] 逢坂美冬, 菊地大介, 上野雄大, 大堀淳, 佐々木加奈子: 関数型言語による高水準な Web アプリ
ケーション開発環境, 富山県教育文化会館, 情報処理学会 第 104 回プログラミング研究発表会,
2015 年 6 月 5 日. (translation: Mifuyu Osaka, Daisuke Kikuchi, Katsuhiro Ueno, Atsushi
Ohori, Kanako Sasaki: A Web application development environment in a functional language.
The 104th meeting of Special Interest Group on Programming (PRO), Information Processing
Society of Japan, June, 2015. )[1-46] 新田祐児, 上野雄大, 大堀淳. 関数型と組型がネストした型を持つ変数を含んだ式の自動生成手法.
情報処理学会プログラミング研究会 第 108 回プログラミング研究発表会, 8 pages, 2016 年 2 月.
(translation: Yuji Nitta, Katsuhiro Ueno, Atsushi Ohori: Automatic generation of expressions
including variables of nested function and tuple types. The 108th meeting of Special Interest
Group on Programming (PRO), Information Processing Society of Japan, February, 2016. )[1-47] 田畑憲太, 上野雄大, 大堀淳. コンパイラ実装言語で中間表現データ構造を記述するための言語機構. 情報処理学会プログラミング研究会 第 108 回プログラミング研究発表会, 5 pages, 2016
年 2 月. (translation: Kenta Tabata, Katsuhiro Ueno, Atsushi Ohori: Approach to writing
an intermediate representation in a language for compiler implementation. The 108th meetingof Special Interest Group on Programming (PRO), Information Processing Society of Japan,
February, 2016. )[1-48] 美馬久行, 上野雄大, 大堀淳. SML#による Vertex-centric プログラミングに向けて. 日本ソフトウェ
ア科学会 第 33 回大会, 2016 年 9 月. (translation: Hisayuki Mima, Katsuhiro Ueno, Atsushi
Ohori: Toward Vertex-centric Programming in SML#, Annual Meeting of the Japan Society
for Software Science and Technology, September, 2016. )[1-49] 逢坂美冬, 上野雄大, 大堀淳. 部分動的レコードを活用した型付きテンプレートエンジンの試作. 日本
ソフトウェア科学会 第 33 回大会, 2016 年 9 月. (translation: Mifuyu Osaka, Katsuhiro Ueno,
Atsushi Ohori: Prototype of a typed template engine using partially-dynamic records, Annual
Meeting of the Japan Society for Software Science and Technology, September, 2016. )[1-50] 徳永航平, 上野雄大, 大堀淳. OS を関数型言語のみで開発するための検討と試作. 日本ソフトウェ
ア科学会 第 33 回大会, 2016 年 9 月. (translation: Kohei Tokunaga, Katsuhiro Ueno, Atsushi
Ohori: Toward developing an OS only in a functional language, Annual Meeting of the Japan
Society for Software Science and Technology, September, 2016. )[1-51] 佐々木智啓, 上野雄大, 大堀淳. 自然結合制約を含む型推論アルゴリズムの実装方式. 日本ソフトウェア科学会 第 33 回大会, 2016 年 9 月. (translation: Tomohiro Sasaki, Katsuhiro Ueno,
Atsushi Ohori: Implementation of a type inference algorithm with natural join constraint,
Annual Meeting of the Japan Society for Software Science and Technology, September, 2016. )[1-52] 佐藤友昭, 上野雄大, 大堀淳. SML ＃のよりシームレスな外部関数インターフェースの実現に向けて. 日本ソフトウェア科学会 第 33 回大会, 2016 年 9 月. (translation: Tomoaki Sato, Katsuhiro
Ueno, Atsushi Ohori: Toward making SML# foreign function interface more seamless, Annual
Meeting of the Japan Society for Software Science and Technology, September, 2016. )[1-53] 美馬久行, 上野雄大, 大堀淳: 多相関数を含むプログラムの抽象解釈を用いた最適化, 日本ソフトウェ
ア科学会第 34 回大会, 慶応義塾大学日吉キャンパス, 2017 年 9 月 21 日. (translation: Hisayuki
Mima, Katsuhiro Ueno, Atsushi Ohori: Optimization for programs including polymorphic functions by abstract interpretation, Annual Meeting of the Japan Society for Software Science andTechnology, September, 2017. )6

[1-54] 大野一樹, 上野雄大, 大堀淳: SML#のためのコードレベルデバッグ環境の構築に向けて, 日本ソ
フトウェア科学会第 34 回大会, 慶応義塾大学日吉キャンパス, 2017 年 9 月 20 日. (translation:
Kazuki Ono, Katsuhiro Ueno, Atsushi Ohori: Toward code-level debugging environment for
SML#, Annual Meeting of the Japan Society for Software Science and Technology, September,2017. )
[1-55] 大塚祐貴, Karim HAMDI, 上野雄大, 大堀淳: 高水準 IoT プログラミング環境の実現に向けて（ポスター発表）, The 2nd. cross-disciplinary Workshop on Computing Systems, Infrastructures,
and Programming (xSIG 2018), 一橋講堂, 2018 年 5 月 29 日. (translation: Yuki Otsuka,
Krim Hamdi, Katsuhiro Ueno, Atsushi Ohori: Toward a high level programming environmentfor IoT, The 2nd. cross-disciplinary Workshop on Computing Systems, Infrastructures, andProgramming (xSIG 2018), May, 2018. )[1-56] 菊池健太郎, 篠埜功: 無限のデータを含む等式に対する帰納的定理証明, 日本ソフトウェア科学会第35 回大会, 大阪大学コンベンションセンター, 2018 年 8 月 30 日. (translation: Kentaro Kikuchi,
Isao Sasano: Inductive Theorem Proving for Equations with Infinite Data. Annual Meeting of
the Japan Society for Software Science and Technology, September, 2018. )(8) 著書 / Books
None(9) 特許 / PatentsNone(10) 招待講演 / Invited Talks[1-57] 大堀淳. 関数型言語 SML#の開発 我が国のソフトウェア産業新生へのささやかな貢献を目指して．
招待講演. 日本ソフトウェア科学会第 30 回大会，東京大学，2013 年 9 月 12 日．(translation:
Atsushi Ohori. Development of the functional language SML# – toward contributing revitalization of Japanese software industry. Keynote speech, The 30th Annual Meeting of the Japan
Society for Software Science and Technology, September, 2013. )[1-58] Katsuhiro Ueno: The SML# compiler backend: compiling ML to C-compatible low-level code,
Syntax and Semantics of Low-Level Languages (LOLA 2015), Invited talk, July, 2015.

2 学会活動 / Activities in academic societies(1) 学会役員等の活動 / Activities on committees of academic societies[2-1] Atsushi Ohori, Conference Chair, The 33rd JSSST (Japan Society for Software Science andTechnology) Annual Conference, 2016[2-2] Katsuhiro Ueno, Organizing Committee Chair, The 33rd JSSST Annual Conference, 2016[2-3] Atsushi Ohori, Councilor of Japan Society for Software Science and Technology, 2004 – present[2-4] Katsuhiro Ueno, Program Committee Member, ACM ICFP, 2018.

7

(2) 学術的国際会議の企画・運営
Planning and organizing academic international conferences
None

3 社会貢献 / Contributions to society(1) 教育活動 / Educational activities outside university
None(2) 産業界における指導・啓蒙 / Instruction and education for industry[3-1] Development of ERP System based on SML#. Research collaboration and consultation to NEC
Software Tohoku, 2012 – 2014.
[3-2] High-level Programming Framework for Highly Available Storage System. Research collaboration and consultation to Hitachi Solutions Higashinihon, 2013 – 2017.

(3) 国・地方自治体・公共団体における活動
Activities for national and local governments, and public organizations[3-3] 大堀 淳、日本学術会議連携会員、2011 年 10 月〜現在 (translation: A member (連携会員) of
Science Council of Japan, Oct. 2011 – present )(4) アウトリーチ活動 / Outreach activities[3-4] 模擬授業「情報の表現と計算の原理」2017 年３月 (translation: “Information Representation andPrinciples of Computing”. Special Lecture for Tsuruoka High School Students. March, 2017.
)[3-5] 出張講義「数理論理学入門：「論理的である」とはどういうことか」鶴岡南高等学校、2017 年 10 月。
(translation: “Introduction to Mathematical Logic: what is the meaning of ‘being logical”’
Special Lecture for Tsuruoka High School Students. October, 2017. )4 競争的資金の獲得状況 / Research funds/grants received(1) 科学研究費補助金 / Grant-in-Aid for Scientific Research (KAKENHI)[4-1] Atsushi Ohori (chief investigator), “Basic research on implementation technology for making
SML# a practical polymorphic language” Grant-in-Aid for Basic Research (B), 2013-4 – 2018-3,
total amount 8,190,000 yen.
[4-2] Atsushi Ohori (chief investigator), “Development of a Massively Parallel Functional Language
by Integrating Massively Parallel Technology into the ML-style polymorphic languageSML#”,
Grant-in-Aid for Basic Research (C), 2018-4 – 2022-3, total amount 4,290,000 yen

8[4-3] Katsuhiro Ueno (chief investigator), “Realizing a systematic infrastructure for practical programming language development”, Grant-in-Aid for Young Scientists (B), 2015-4 – 2019-3,
total amount: 3,900,000 yen[4-4] Katsuhiro Ueno (chief investigator), “A study on high-level and safe interoperability of programming languages” Grant-in-Aid for Young Scientists (B), 2012-4 – 2015-3, total amount:
2,730,000 yen[4-5] Kentaro Kikuchi (chief investigator), “Program Verification Methods based on Context-Moving
Transformation and Higher-Order Rewriting Theory”, Grant-in-Aid for Scientific Research (C),2016-4 – 2019-3, total amount 3,510,000 yen(2) 受託研究費 / Other grants and subsidies[4-6] “Application of reliable programming language to system development” 2013-1 – 2014-3 research
Fund received from NEC Tohoku, total amount 1,363,132 yen.
[4-7] “High-level Programming Framework for Highly Available Storage System” Contract researcher
Kikuchi Daisuke from Hitachi Solutions Higashinihon, 2014-11 – 2015-3, total amount 232,000yen.
[4-8] “High-level Programming Framework for Highly Available Storage System” Contract researcher
Kikuchi Daisuke from Hitachi Solutions Higashinihon, 2015-4 – 2016-3, total amount 464,000
yen.

5 国際共同研究・連携研究・連携教育活動の実績/ International joint
research, collaborative research, and collaborative education
6 研究教育指導 / Research supervision(1) 担当講義リスト / List of lectures
1. Lectures in undergraduate schools （Course title Year Instructor）• Compiler, 2013 – 2018, Atsushi Ohori• System Software Engineering, 2013〜2018, Atsushi Ohori jointly with one professor.
• Team-based Engineering Design Course 2013 - 2018 Katsuhiro Ueno
• Programming Course B, 2013 - 2018 Katsuhiro Ueno with 3 other people• Basic seminar for first year undergraduate students, 2013 - 2018, Atsushi Ohori jointly with
5 professors.
2. Lectures in graduate schools （Course title Year Instructor）• Software Construction 2013 - 2018 Atsushi Ohori and Katsuhiro Ueno (from 2018 –)(2) 学位取得者リスト// List of bachelor’s, master’s and doctoral degree students supervised
1. 学部卒業論文/List of bachelor’s degree• 早下雅弘「自然言語の意味解析処理のためのプログラミング基盤の研究」2019 年 3 月 (translation: Masahiro Hayashita, “A Study on programming environment for semantic processingof natural languages”, 2019-3. )9• 山崎 岳「データからのテンプレート自動生成に関する研究」2019 年 3 月 (translation: Gaku
Yamazaki, “A Study on automatic template generation from data” 2019-3. )• 魚谷 孝太「Java PathFinder?による ML プログラムの捕捉されない例外の検証の研究」2018
年 3 月 (translation: Kota Uotani, “A study on analyzing uncaught exception using Java
PathFinder” 2018-3. )• 大塚 祐貴「高水準言語のための IoT プログラミング環境の研究」2018 年 3 月 (translation:
Yuki Otuka, “A study on IoT programming environment for high-level languages” 2018-3.
)• 高城 光平「ML 系言語とストリーミングデータベースの統合に関する研究」2018 年 3 月(translation: Kohei Takagi “A study on integrating streaming databases into an ML-stylelanguage” 2018-3. )• 佐々木 雄哉「SML#の JSON サポートを基礎とした Web リクエストデータの静的型付けの研究」2017 年 3 月 (translation: Yuya Sasaki, “A study on static typing of Web request data
based on SML# JSON support” 2017-3. )• 橋本 航汰「関数型言語向け高水準 web サーバー開発環境のためのユーザー認証システム」
2017 年 3 月 (translation: Kota Hashimoto, “A user authentication system for a functional
language web server” 2017-3. )• 大野 一樹「高信頼 Web プログラミングのためのテンプレートエンジンに関する研究」2016
年 3 月 (translation: Kazuki Ono “A study on template engine for highly reliable web
programming” 2016-3. )• 徳永 航平「OS のサポート無しに関数型言語のプログラムを動かすための実装方式」2016 年 3
月 (translation: Kohei Tokunaga, “A method for running a functional language program
without OS support” 2016-3. )• 逢坂 美冬「関数型言語における Web 技術を用いた高機能な情報表示方式の研究」2015 年 3
月 (translation: Mifuyu Osaka, “A study on high-level data representation method forfunctional languages based on Web technologies” 2015-3. )• 佐々木 智啓「関数型言語への自然結合の導入方式」2015 年 3 月 (translation: Tomoaki Sasaki,“Introduction of Natural Join to a functional language”, 2015-3. )• 田畑 憲太「SML#への並列コンピューティングのためのインターフェイスの導入」2014 年 3 月(translation: Kenta Tabata, “Introducing parallel computing interface to SML#”, 2014-3.
)• 新田 祐児「型推論による不完全な構文を含んだプログラムの補完支援」2014 年 3 月 (translation: Yuji Nitta, “Completing assistance for incomplete program based on type inference”,
2014-3. )2. 修士学位論文/List of master’s degree• Yuya Sasaki, “A Study on Technology
to Construct Secure Client-side in Web Applications” 2019-3. (in Japanese)• Kota Hashimoto, “A Study on a High-level Declarative Image Processing Programming
Environment with SML# and OpenCV”, 2019-3. (in Japanese)• Hisayuki Mima, “A Study on Static Analysis for Optimizing Polymorphic Languages” 20183.
• Kazuki Ono, “A Study on Code Level Debugging Environment for Functional Languages”,
2018-3. (in Japanese)• Kohei Tokunaga, “A Study on Developing a Functional Language for Describing Operating
Systems”, 2018-3. (in Japanese)10• Mifuyu OSAKA, “Developing a Web Application Developing Environment with Type System and Compiling Method”, 2017-3. (in Japanese)• Tomohiro Sasaki, “A Study on Integrating Natural Join into a ML-style Programming
Language”, 2017-3.
• Tomoaki SATO “Implementation of a More Complete and Convenient Foreign Function
Calling Method”, 2017-3. (in Japanese)• Kenta Tabata. “A study on representing and manipulating compiler intermediate languages” 2016-3.
• Yuji Nitta, “A study on systematic testing method for functional languages” 2016-3.
• Masanori Endo, “A study on static typing for resource identity”, 2015-3.
• Yuto Mukade, “A study on compiler support for functional program understanding”, 20153.
• Hikaru Saito, “A study on integrating advanced SQL features in a functional language”,
2014-3.
• Yutaka Fukasawa, “A study on formal semantics of Ruby”, 2014-3.
3. 博士学位論文/List of doctor’s degree• 相澤 正俊「オープンミッションクリティカルシステム構築技術の研究」2013 年７月（論文博士）(translation: Masatoshi Aizawa, “A study on open mission critical system development
methodology” 2013-7. (Doctoral Degree by Dissertation) )7 叙勲・受賞・表彰 / Honors, awards, and prizes[7-1] 上野雄大、トーキン財団奨励賞、高信頼プログラミング言語の実用化技術の研究および次世代

言語処理系の開発、平成２６年３月 (translation: Katsuhiro Ueno, Tokin foundation award,“Implementation methodology for reliable programming languages and development of a nextgeneration programming language system”, 2014-3. )[7-2] Best Review Paper Award, “Principles of LR Parsing” (in Japanese), Computer Software, vol31,
no 1, 2016.
[7-3] 大堀 淳、平成２９年度 日本学術振興会 審査委員表象 (translation: Atsushi Ohori, Recognitionof Excellent Evaluation Committee Member of JSPS Kakenhi Grant, 2017. )8 その他 / Others[8–1]「高信頼言語と形式仕様言語を並列処理系上に統合する高性能高信頼ソフトウェア生産基盤」（本計画
に関する連絡先：大堀 淳）日本学術会議 提言 第 23 期学術の大型研究計画に関するマスタープラン（マスタープラン 2017），計画番号 86，学術領域番号 25-2，2017 年 2 月(translation: “Development of software production infrastructure by integrating reliable programming languages and specification languages on massively parallel programming environment” (contact: Atsushi Ohori) Recommendation : Japanese Master Plan of Large Research
Projects, Science Council of Japan, February, 2017. )[8–2]「高信頼プログラミング言語と代数仕様記述言語を統合した高信頼ソフトウエア工学基盤」（本計画に関する連絡先：大堀 淳）日本学術会議 提言 第 22 期学術の大型研究計画に関するマスタープラン（マスタープラン 2014），計画番号 115 学術領域番号 25-2，2014 年 2 月.
11(translation: “Development of software production infrastructure by integrating reliable programming languages and algebraic specification languages” (contact: Atsushi Ohori) Recommendation : Japanese Master Plan of Large Research Projects, Science Council of Japan,
February, 2017. )12