• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Research on software contracts for highly interoperable software modules

Research Project

Project/Area Number 20H00582
Research Category

Grant-in-Aid for Scientific Research (A)

Allocation TypeSingle-year Grants
Section一般
Review Section Medium-sized Section 60:Information science, computer engineering, and related fields
Research InstitutionKyoto University

Principal Investigator

五十嵐 淳  京都大学, 情報学研究科, 教授 (40323456)

Co-Investigator(Kenkyū-buntansha) 末永 幸平  京都大学, 情報学研究科, 准教授 (70633692)
池渕 未来  京都大学, 情報学研究科, 助教 (70961796)
関山 太朗  国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
田邉 裕大  東京工業大学, 情報理工学院, 助教 (30985198)
松下 祐介  京都大学, 情報学研究科, 特別研究員(PD) (41003875)
Project Period (FY) 2020-04-01 – 2025-03-31
Project Status Granted (Fiscal Year 2024)
Budget Amount *help
¥44,460,000 (Direct Cost: ¥34,200,000、Indirect Cost: ¥10,260,000)
Fiscal Year 2024: ¥8,450,000 (Direct Cost: ¥6,500,000、Indirect Cost: ¥1,950,000)
Fiscal Year 2023: ¥8,840,000 (Direct Cost: ¥6,800,000、Indirect Cost: ¥2,040,000)
Fiscal Year 2022: ¥8,840,000 (Direct Cost: ¥6,800,000、Indirect Cost: ¥2,040,000)
Fiscal Year 2021: ¥8,840,000 (Direct Cost: ¥6,800,000、Indirect Cost: ¥2,040,000)
Fiscal Year 2020: ¥9,490,000 (Direct Cost: ¥7,300,000、Indirect Cost: ¥2,190,000)
Keywordsプログラミング言語 / プログラム検証 / 相互運用性 / ソフトウェア契約 / ソフトウエア契約
Outline of Research at the Start

近年のソフトウェアシステムは、プログラミング言語に対して言語間相互運用性を要請することが多くなっている。しかし、言語間相互運用性を活用しつつ、正しく動くソフトウェアを構築するのは、単一の言語でのソフトウェア開発よりもさらに困難である。我々は「言語間相互運用を活用したソフトウェアシステムを正しく構築するための技術はどうあるべきか」を研究課題の核心をなす学術的「問い」として据え、ソフトウェア契約というソフトウェア検証のための方法論を、言語間相互運用性とシステムの高信頼性を確保するための技術として拡張・発展させる研究を行う。

Outline of Annual Research Achievements

本年度は、交付申請書時点で計画したふたつの研究項目のうち、【研究項目2. 多言語モジュールで構成されたソフトウェアシステムの検証機構】 の(項目2-2)、多相型を持つ言語と動的型付言語間の相互運用を行うための実行検査について効率的な実装のための技術の検討に大半の時間を費した。当初、前年度までの, 「完全に空間効率がよい実装は不可能ではあるが、ある意味でほとんど空間効率のよい実装であれば可能」という理論的な結果を洗練させる予定であったが、研究を進める中で、多相関数に与えられる型引数が動的型である場合のみパラメトリシティ性を諦めることで、完全に空間効率がよい実装が可能であることに気付いたため、その実装技術の理論化を行い論文にまとめた(発表予定)。(項目2-1)の「データ変換を行う仕組みと実行時検査機構を組み合わせる手法の検討」については関連研究のサーベイなどを進めた。

【研究項目1. モジュール間のデータ変換機構とその自動化の研究】 については、レコードとハッシュテーブルが相互運用可能な言語のプロトタイプの完成を目指した。前年度までの研究で判明した、再帰的データ構造を扱う際の理論的な課題について取り組んだが、前年度までに研究協力者であった大学院生の修了もあり、解決には至らなかった。一方で、この方式をレコードとハッシュテーブルの組み合わせに限らず一般化する理論の検討を行った。この一般化により、例えば、ハッシュテーブルを文字列を受け取って(動的型の)値を返す関数とみなし、関数適用の構文を使ってハッシュテーブルの値を読み出すことが可能になると考えている。ただし、どういった組み合わせならば相互運用が可能なのかについてはまだ不明なところも多い。

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

個別の研究項目については、項目2-2の、多相型を持つ言語と動的型付言語間の相互運用を行うための空間効率のよい実行検査の研究のように想定以上の進展があったものと、やや遅れているもの(項目1と項目2-1)が混在しているが、全体的には「おおむね順調」と判断した。

項目1と項目2-1の遅れは、項目2-2の研究を進める間に生じた理論的な問題を解消するのに数ヶ月を費したために当初想定していた時間がかけられなかったことと、研究協力者の不在が主な原因である。

Strategy for Future Research Activity

雇用していたポスドクが次の職を得て離れてしまうが研究分担者としては残ること、また、今年度時間を費した項目2-2の研究については一段落つくので、遅れている項目について、学生の研究協力者も加え研究を加速させる。

Report

(4 results)
  • 2022 Annual Research Report
  • 2021 Annual Research Report
  • 2020 Comments on the Screening Results   Annual Research Report
  • Research Products

    (31 results)

All 2024 2023 2022 2021 2020 Other

All Int'l Joint Research (1 results) Journal Article (13 results) (of which Peer Reviewed: 10 results,  Open Access: 10 results) Presentation (16 results) (of which Int'l Joint Research: 8 results,  Invited: 2 results) Remarks (1 results)

  • [Int'l Joint Research] フライブルク大学(ドイツ)

    • Related Report
      2021 Annual Research Report
  • [Journal Article] Space-Efficient Polymorphic Gradual Typing, Mostly Parametric2024

    • Author(s)
      Atsushi Igarashi, Shota Ozaki, Taro Sekiyama, Yudai Tanabe
    • Journal Title

      Proceedings of the ACM on Programming Languages (PLDI)

      Volume: - Issue: PLDI Pages: 1585-1608

    • DOI

      10.1145/3656441

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] An ML-Style Module System for Cross-Stage Type Abstraction in Multi-Stage Programming2024

    • Author(s)
      Takashi Suwa, Atsushi Igarashi
    • Journal Title

      Proc. of FLOPS 2024

      Volume: ー

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024

    • Author(s)
      Kawamata Fuga, Unno Hiroshi, Sekiyama Taro, Terauchi Tachio
    • Journal Title

      Proceedings of the ACM on Programming Languages (POPL)

      Volume: 8 Issue: POPL Pages: 115-147

    • DOI

      10.1145/3633280

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Contextual Modal Type Theory with Polymorphic Contexts2023

    • Author(s)
      Yuito Murase, Yuichi Nishiwaki, Atsushi Igarashi
    • Journal Title

      Proc. of ESOP 2023

      Volume: 13990 Pages: 281-308

    • DOI

      10.1007/978-3-031-30044-8_11

    • ISBN
      9783031300431, 9783031300448
    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Formalizing Statistical Causality via Modal Logic2023

    • Author(s)
      Kawamoto Yusuke、Sato Tetsuya、Suenaga Kohei
    • Journal Title

      Logics in Artificial Intelligence: 18th European Conference, JELIA 2023, Dresden, Germany, September 20-22, 2023, Proceedings

      Volume: - Pages: 681-696

    • DOI

      10.1007/978-3-031-43619-2_46

    • ISBN
      9783031436185, 9783031436192
    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations2023

    • Author(s)
      Sekiyama Taro、Unno Hiroshi
    • Journal Title

      Proceedings of the ACM on Programming Languages

      Volume: 7 Issue: POPL Pages: 2079-2110

    • DOI

      10.1145/3571264

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ2023

    • Author(s)
      臼澤嘉, 末永幸平, 古瀬淳, 五十嵐淳
    • Journal Title

      第25回プログラミングおよびプログラミング言語ワークショップ(PPL2023)論文集

      Volume: ー

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Stage-Aware Equality Types for a Dependently-Typed Multi-Stage Calculus2022

    • Author(s)
      Shuntaro Katsuda, Atsushi Igarashi
    • Journal Title

      第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集

      Volume: ー

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Type-based Qubit Allocation for a First-Order Quantum Programming Language2022

    • Author(s)
      Ryo Wakizaka, Atsushi Igarashi
    • Journal Title

      第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)論文集

      Volume: ー

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法2022

    • Author(s)
      梅木 孝輔, 関山 太朗, 五十嵐 淳
    • Journal Title

      日本ソフトウェア科学会第39回大会論文集

      Volume: ー

    • Related Report
      2021 Annual Research Report
    • Open Access
  • [Journal Article] CPS transformation with affine types for call-by-value implicit polymorphism2021

    • Author(s)
      Sekiyama Taro、Tsukada Takeshi
    • Journal Title

      Proceedings of the ACM on Programming Languages (ICFP)

      Volume: 5 Issue: ICFP Pages: 1-30

    • DOI

      10.1145/3473600

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Is Space-Efficient Polymorphic Gradual Typing Possible?2021

    • Author(s)
      Shota Ozaki, Taro Sekiyama, Atsushi Igarashi
    • Journal Title

      Informal Proceedings of Scheme and Functional Programming Workshop

      Volume: ー

    • Related Report
      2020 Annual Research Report
    • Open Access
  • [Journal Article] Compilation of Coordinated Choice2020

    • Author(s)
      Yuki Nishida, Atsushi Igarashi
    • Journal Title

      arXiv

      Volume: ー

    • Related Report
      2020 Annual Research Report
    • Open Access
  • [Presentation] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024

    • Author(s)
      Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
    • Organizer
      ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Contextual Modal Type Theory with Polymorphic Contexts2023

    • Author(s)
      Yuito Murase, Yuichi Nishiwaki, Atsushi Igarashi
    • Organizer
      European Symposium on Programming
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2023

    • Author(s)
      Taro Sekiyama
    • Organizer
      Shonan Meeting (No. 203)
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research / Invited
  • [Presentation] Formalizing Statistical Causality via Modal Logic2023

    • Author(s)
      Yusuke Kawamoto and Tetsuya Sato and Kohei Suenaga
    • Organizer
      JELIA
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations2023

    • Author(s)
      Taro Sekiyama, Hiroshi Unno
    • Organizer
      ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 代数的エフェクトとハンドラのためのエフェクトシステムの抽象化2023

    • Author(s)
      吉岡 拓真, 関山 太朗, 五十嵐 淳
    • Organizer
      第25回プログラミングおよびプログラミング言語ワークショップ(PPL 2023)
    • Related Report
      2021 Annual Research Report
  • [Presentation] 限定継続のための高階プログラム論理2023

    • Author(s)
      佐藤 惇, 関山 太朗, 五十嵐 淳
    • Organizer
      第25回プログラミングおよびプログラミング言語ワークショップ(PPL 2023)
    • Related Report
      2021 Annual Research Report
  • [Presentation] 代数的エフェクトハンドラのための篩型システム2023

    • Author(s)
      川俣 楓河, 海野 広志, 関山 太朗, 寺内 多智弘
    • Organizer
      第25回プログラミングおよびプログラミング言語ワークショップ(PPL 2023)
    • Related Report
      2021 Annual Research Report
  • [Presentation] Stage-Aware Equality Types for a Dependently-Typed Multi-Stage Calculus2022

    • Author(s)
      Shuntaro Katsuda, Atsushi Igarashi
    • Organizer
      第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)
    • Related Report
      2021 Annual Research Report
  • [Presentation] Type-based Qubit Allocation for a First-Order Quantum Programming Language2022

    • Author(s)
      Ryo Wakizaka, Atsushi Igarashi
    • Organizer
      第24回プログラミングおよびプログラミング言語ワークショップ(PPL2022)
    • Related Report
      2021 Annual Research Report
  • [Presentation] 分岐付き確率的プログラミング言語の実現に向けて2022

    • Author(s)
      兼光 琢真, 関山 太朗
    • Organizer
      第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)
    • Related Report
      2021 Annual Research Report
  • [Presentation] 計算効果入門 ― プログラミングから理論まで ―2022

    • Author(s)
      関山 太朗、勝股 審也、叢 悠悠
    • Organizer
      PPLサマースクール2022
    • Related Report
      2021 Annual Research Report
    • Invited
  • [Presentation] CPS transformation with affine types for call-by-value implicit polymorphism2021

    • Author(s)
      Taro Sekiyama, Takeshi Tsukada
    • Organizer
      ACM SIGPLAN International Conference on Functional Programming (ICFP)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Is Space-Efficient Polymorphic Gradual Typing Possible?2021

    • Author(s)
      Shota Ozaki, Taro Sekiyama, Atsushi Igarashi
    • Organizer
      Scheme and Functional Programming Workshop
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] レコードとハッシュテーブルの暗黙な相互運用を可能にする型推論とコンパイル手法2021

    • Author(s)
      梅木孝輔, 関山太朗, 五十嵐淳
    • Organizer
      第23回プログラミングおよびプログラミング言語ワークショップ(PPL2021)
    • Related Report
      2020 Annual Research Report
  • [Presentation] Space-Efficient Gradual Typing in Coercion-Passing Style2020

    • Author(s)
      Yuya Tsuda, Atsushi Igarashi, Tomoya Tabuchi
    • Organizer
      European Conference on Object-Oriented Programming (ECOOP2020)
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Remarks] 五十嵐淳ホームページ

    • URL

      https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/

    • Related Report
      2022 Annual Research Report 2021 Annual Research Report 2020 Annual Research Report

URL: 

Published: 2020-04-28   Modified: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi