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

2022 Fiscal Year Annual Research Report

Research on software contracts for highly interoperable software modules

Research Project

Project/Area Number 20H00582
Research InstitutionKyoto University

Principal Investigator

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

Co-Investigator(Kenkyū-buntansha) 末永 幸平  京都大学, 情報学研究科, 准教授 (70633692)
関山 太朗  国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
Project Period (FY) 2020-04-01 – 2025-03-31
Keywordsプログラミング言語 / プログラム検証 / 相互運用性 / ソフトウェア契約
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の研究については一段落つくので、遅れている項目について、学生の研究協力者も加え研究を加速させる。

  • Research Products

    (10 results)

All 2024 2023 Other

All Journal Article (5 results) (of which Peer Reviewed: 5 results,  Open Access: 4 results) Presentation (4 results) (of which Int'l Joint Research: 4 results,  Invited: 1 results) Remarks (1 results)

  • [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: ー Pages: ー

    • DOI

      10.1145/3656441

    • 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: ー Pages: ー

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

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

      Proceedings of the ACM on Programming Languages (POPL)

      Volume: 8 Pages: 115-147

    • DOI

      10.1145/3633280

    • 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

    • Peer Reviewed / Open Access
  • [Journal Article] Formalizing Statistical Causality via Modal Logic2023

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

      Proceedings of JELIA 2023

      Volume: 14281 Pages: 681-696

    • DOI

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

    • Peer Reviewed
  • [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)
    • 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
    • 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)
    • Int'l Joint Research / Invited
  • [Presentation] Formalizing Statistical Causality via Modal Logic2023

    • Author(s)
      Yusuke Kawamoto and Tetsuya Sato and Kohei Suenaga
    • Organizer
      JELIA
    • Int'l Joint Research
  • [Remarks] 五十嵐淳ホームページ

    • URL

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

URL: 

Published: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi