Development of theory and application of programming based on higher-order/typed calculi

• Project/Area Number: 15H02681
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Tohoku University
• Principal Investigator: Sumii Eijiro 東北大学, 情報科学研究科, 教授 (00333550)
• Project Period (FY): 2015-04-01 – 2020-03-31
• Project Status: Completed (Fiscal Year 2019)
• Budget Amount: ¥17,810,000 (Direct Cost: ¥13,700,000、Indirect Cost: ¥4,110,000); Fiscal Year 2019: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000); Fiscal Year 2018: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000); Fiscal Year 2017: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000); Fiscal Year 2016: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000); Fiscal Year 2015: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
• Keywords: プログラミング言語理論 / 関数型プログラミング / 高階計算・λ計算（ラムダ計算） / 型システム / 情報セキュリティ・情報流解析 / 並行・分散計算 / 形式的（機械的）定理証明・検証 / 環境双模倣 / セキュリティ / 並行計算 / ソフトウェア基礎 / 関数型言語 / 必要呼び評価戦略 / 関数型プログラミング言語 / セキュリティ型つきλ計算 / 非機密化(declassification) / 遅延評価 / 名前呼び / 必要呼び / プログラム検証 / 評価戦略 / λ計算 / セキュリティ型 / declassification / 秘密性・機密性 / プログラム等価性

Outline of Final Research Achievements

As enumerated in the report, a variety of results and new theories have been obtained by developing and applying programming language theory (in particular, higher-order computation and static type systems) studied in functional languages and related research fields. Some of our research has been accepted as full papers and presented in refereed, high-quality international conferences.

Academic Significance and Societal Importance of the Research Achievements

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

Research Products

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