• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2022 年度 実績報告書

高相互運用性を持つソフトウェアモジュールのためのソフトウェア契約の研究

研究課題

研究課題/領域番号 20H00582
研究機関京都大学

研究代表者

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

研究分担者 末永 幸平  京都大学, 情報学研究科, 准教授 (70633692)
関山 太朗  国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
研究期間 (年度) 2020-04-01 – 2025-03-31
キーワードプログラミング言語 / プログラム検証 / 相互運用性 / ソフトウェア契約
研究実績の概要

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

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

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

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

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

今後の研究の推進方策

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

  • 研究成果

    (10件)

すべて 2024 2023 その他

すべて 雑誌論文 (5件) (うち査読あり 5件、 オープンアクセス 4件) 学会発表 (4件) (うち国際学会 4件、 招待講演 1件) 備考 (1件)

  • [雑誌論文] Space-Efficient Polymorphic Gradual Typing, Mostly Parametric2024

    • 著者名/発表者名
      Atsushi Igarashi, Shota Ozaki, Taro Sekiyama, Yudai Tanabe
    • 雑誌名

      Proceedings of the ACM on Programming Languages (PLDI)

      巻: ー ページ: ー

    • DOI

      10.1145/3656441

    • 査読あり / オープンアクセス
  • [雑誌論文] An ML-Style Module System for Cross-Stage Type Abstraction in Multi-Stage Programming2024

    • 著者名/発表者名
      Takashi Suwa, Atsushi Igarashi
    • 雑誌名

      Proc. of FLOPS 2024

      巻: ー ページ: ー

    • 査読あり / オープンアクセス
  • [雑誌論文] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024

    • 著者名/発表者名
      Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
    • 雑誌名

      Proceedings of the ACM on Programming Languages (POPL)

      巻: 8 ページ: 115-147

    • DOI

      10.1145/3633280

    • 査読あり / オープンアクセス
  • [雑誌論文] Contextual Modal Type Theory with Polymorphic Contexts2023

    • 著者名/発表者名
      Yuito Murase, Yuichi Nishiwaki, Atsushi Igarashi
    • 雑誌名

      Proc. of ESOP 2023

      巻: 13990 ページ: 281-308

    • DOI

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

    • 査読あり / オープンアクセス
  • [雑誌論文] Formalizing Statistical Causality via Modal Logic2023

    • 著者名/発表者名
      Yusuke Kawamoto and Tetsuya Sato and Kohei Suenaga
    • 雑誌名

      Proceedings of JELIA 2023

      巻: 14281 ページ: 681-696

    • DOI

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

    • 査読あり
  • [学会発表] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024

    • 著者名/発表者名
      Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
    • 学会等名
      ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)
    • 国際学会
  • [学会発表] Contextual Modal Type Theory with Polymorphic Contexts2023

    • 著者名/発表者名
      Yuito Murase, Yuichi Nishiwaki, Atsushi Igarashi
    • 学会等名
      European Symposium on Programming
    • 国際学会
  • [学会発表] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2023

    • 著者名/発表者名
      Taro Sekiyama
    • 学会等名
      Shonan Meeting (No. 203)
    • 国際学会 / 招待講演
  • [学会発表] Formalizing Statistical Causality via Modal Logic2023

    • 著者名/発表者名
      Yusuke Kawamoto and Tetsuya Sato and Kohei Suenaga
    • 学会等名
      JELIA
    • 国際学会
  • [備考] 五十嵐淳ホームページ

    • URL

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

URL: 

公開日: 2024-12-25  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi