高階・型付きの計算体系に基づくプログラミングの理論と応用の展開

• 研究課題/領域番号: 15H02681
• 研究種目: 基盤研究(B)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウェア
• 研究機関: 東北大学
• 研究代表者: 住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
• 研究期間 (年度): 2015-04-01 – 2020-03-31
• 研究課題ステータス: 完了 (2019年度)
• 配分額: 17,810千円 (直接経費: 13,700千円、間接経費: 4,110千円); 2019年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円); 2018年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円); 2017年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円); 2016年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円); 2015年度: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
• キーワード: プログラミング言語理論 / 関数型プログラミング / 高階計算・λ計算（ラムダ計算） / 型システム / 情報セキュリティ・情報流解析 / 並行・分散計算 / 形式的（機械的）定理証明・検証 / 環境双模倣 / セキュリティ / 並行計算 / ソフトウェア基礎 / 関数型言語 / 必要呼び評価戦略 / 関数型プログラミング言語 / セキュリティ型つきλ計算 / 非機密化(declassification) / 遅延評価 / 名前呼び / 必要呼び / プログラム検証 / 評価戦略 / λ計算 / セキュリティ型 / declassification / 秘密性・機密性 / プログラム等価性

研究成果の概要

主に関数型言語ないしそれに近い研究コミュニティで発展してきた，プログラミング言語理論（特に高階計算および静的型システム）をさらに発展・応用することにより，研究成果報告書の本文に列挙のとおり，多岐にわたる成果や新たな理論を得た．研究の一部は，コンピュータサイエンス分野で重要視される，水準の高い査読付国際会議にフルペーパーが採択・発表されるなど，良い評価を得た．

研究成果の学術的意義や社会的意義

広義の「計算」の記述としての高水準プログラミング，ひいては情報処理システムの生産性・信頼性を向上させる分野の研究成果である．研究計画に明記したとおり，本研究は学術的基礎理論研究であり，「201X年YY月にZZZZ理論を着想する」といった具体的計画をあらかじめ立てることはあり得ないため，研究計画もあくまで例示である旨を明記した上で採択されたが，研究題目に沿った多数の予見し得なかった成果が得られ，研究者自身の発想による自由な研究の重要性が再確認された．

研究成果

• [雑誌論文] Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion (2019)
  • 著者名/発表者名: Masayuki Mizuno, Eijiro Sumii
  • 雑誌名: Lecture Notes in Computer Science 巻: 11893 ページ: 181-201
  • DOI: 10.1007/978-3-030-34175-6_10
  • ISBN: 9783030341749, 9783030341756
  • 査読あり
• [雑誌論文] Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name (2018)
  • 著者名/発表者名: Masayuki Mizuno, Eijiro Sumii
  • 雑誌名: Lecture Notes in Computer Science 巻: 10818 ページ: 1-16
  • DOI: 10.1007/978-3-319-90686-7_1
  • ISBN: 9783319906850, 9783319906867
  • 査読あり / オープンアクセス
• [雑誌論文] Formal Verification of the Correspondence between Call-by-Need and Call-by-Name (2018)
  • 著者名/発表者名: Masayuki Mizuno, Eijiro Sumii
  • 雑誌名: Functional and Logic Programming: 14th International Symposium, FLOPS 2018 巻: 印刷中
  • 査読あり / オープンアクセス
• [雑誌論文] Specialization of Generic Array Accesses After Inlining (2017)
  • 著者名/発表者名: Ryohei Tokuda, Eijiro Sumii, Akinori Abe
  • 雑誌名: Proceedings ML Family / OCaml Users and Developers workshops, ML Family/OCaml 2015, Vancouver, Canada, 3rd & 4th September 2015, Electronic Proceedings in Theoretical Computer Science 巻: 241 ページ: 45-53
  • DOI: 10.4204/eptcs.241.4
  • 査読あり / オープンアクセス / 謝辞記載あり
• [雑誌論文] 無限の入出力を行う関数型プログラムのK正規化の形式的検証 (2017)
  • 著者名/発表者名: 水野 雅之, 住井 英二郎
  • 雑誌名: コンピュータソフトウェア 巻: 印刷中
  • NAID: 130006855251
  • 査読あり
• [雑誌論文] A Sound and Complete Bisimulation for Contextual Equivalence in λ-Calculus with Call/cc (2016)
  • 著者名/発表者名: Taichi Yachi, Eijiro Sumii
  • 雑誌名: Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, Lecture Notes in Computer Science 巻: 10017 ページ: 171-186
  • DOI: 10.1007/978-3-319-47958-3_10
  • ISBN: 9783319479576, 9783319479583
  • 査読あり / 謝辞記載あり
• [雑誌論文] A Simple and Practical Linear Algebra Library Interface with Static Size Checking (2015)
  • 著者名/発表者名: Akinori Abe, Eijiro Sumii
  • 雑誌名: EPTCS 巻: 198 ページ: 1-21
  • DOI: 10.4204/eptcs.198.1
  • 査読あり / オープンアクセス / 謝辞記載あり
• [雑誌論文] Specialization of Generic Array Accesses After Inlining (2015)
  • 著者名/発表者名: Ryohei Tokuda, Eijiro Sumii
  • 雑誌名: The OCaml Users and Developers Workshop (talk abstracts) 巻: 2015 ページ: 1-2
  • 査読あり / オープンアクセス / 謝辞記載あり
• [雑誌論文] Call/ccを含む型無しラムダ計算における文脈等価性の一証明手法 (2015)
  • 著者名/発表者名: 谷内太一，住井英二郎
  • 雑誌名: 日本ソフトウェア科学会第32回大会(2015年度)講演論文集 巻: 2015 ページ: 1-7
  • NAID: 40020657231
• [学会発表] Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion (2019)
  • 著者名/発表者名: Masayuki Mizuno, Eijiro Sumii
  • 学会等名: APLAS 2019
  • 国際学会
• [学会発表] Progress report: Ruby 3における静的型解析の実現に向けて (2019)
  • 著者名/発表者名: 遠藤 侑介, 松本 宗太郎, 上野 雄大, 住井 英二郎, 松本 行弘
  • 学会等名: 第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）
• [学会発表] NetKAT with Cryptography (2019)
  • 著者名/発表者名: 菅原 慎之介, 住井 英二郎
  • 学会等名: 第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）
• [学会発表] ブロックチェーン合意形成プロトコルのCoqによる証明からのコード抽出 (2019)
  • 著者名/発表者名: 木村 朝輝, 住井 英二郎
  • 学会等名: 第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）
• [学会発表] Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name (2018)
  • 著者名/発表者名: Masayuki Mizuno, Eijiro Sumii
  • 学会等名: Fourteenth International Symposium on Functional and Logic Programming (FLOPS 2018)
  • 国際学会
• [学会発表] A Sound and Complete Bisimulation for Contextual Equivalence in λ-Calculus with Call/cc (2016)
  • 著者名/発表者名: Taichi Yachi, Eijiro Sumii
  • 学会等名: 14th Asian Symposium on Programming Languages and Systems
  • 発表場所: Hanoi, Vietnam
  • 年月日: 2016-11-21
  • 国際学会
• [学会発表] 無限の入出力を行う関数型プログラムのK正規化の形式的検証 (2016)
  • 著者名/発表者名: 水野 雅之, 住井 英二郎
  • 学会等名: 日本ソフトウェア科学会大会
  • 発表場所: 東北大学（仙台市）
  • 年月日: 2016-09-09
• [学会発表] 機械学習による関数型ブーリアンプログラムの型推論 (2016)
  • 著者名/発表者名: 阿部 晃典，住井 英二郎
  • 学会等名: 第18回プログラミングおよびプログラミング言語ワークショップ（PPL2016）
  • 発表場所: ダイヤモンド瀬戸内マリンホテル（岡山県玉野市）
  • 年月日: 2016-03-07
• [学会発表] Call/ccを含む型無しラムダ計算における文脈等価性の一証明手法 (2015)
  • 著者名/発表者名: 谷内太一，住井英二郎
  • 学会等名: 日本ソフトウェア科学会第32回大会
  • 発表場所: 早稲田大学西早稲田キャンパス（東京都新宿区）
  • 年月日: 2015-09-10
• [学会発表] Specialization of Generic Array Accesses After Inlining (2015)
  • 著者名/発表者名: Ryohei Tokuda, Eijiro Sumii
  • 学会等名: The OCaml Users and Developers Workshop
  • 発表場所: Vancouver, Canada
  • 年月日: 2015-09-04
  • 国際学会
• [備考] Sized Linear Algebra Package (SLAP)
  • URL: http://akabe.github.io/slap/