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

2018 年度 実績報告書

ゲーム意味論と交差型システムによるプログラム検証

研究課題

研究課題/領域番号 16K16004
研究機関東京大学

研究代表者

塚田 武志  東京大学, 大学院情報理工学系研究科, 助教 (50758951)

研究期間 (年度) 2016-04-01 – 2019-03-31
キーワードプログラム意味論 / ゲーム意味論 / 交差型システム / generalised species / 線形論理
研究実績の概要

本研究は関数型プログラミング言語のモデルであるλ計算について「ゲーム意味論と交差型システムの対応関係」を確立し、得られた知見を基に並行計算のモデルであるπ計算の交差型システムを設計した上で検証等へ応用するものであった。
(1) λ計算のモデルについて、前年度に得られた結果をさらに発展させ、非決定性プログラム・確率的プログラム・量子的プログラムなどを一様に扱うことのできる意味論の枠組みを与えることに成功した。この枠組は、通常の交差型システムの一般化であること理解することができ、「型が付くか否か」という質的な情報だけではなく、「どの程度型が付くのか」という量的な情報を扱うことができるものである。量的な情報を交差型システムを利用して記述する手法については多くの先行研究があるが、本成果は扱える量的な情報のクラスを非常に一般的な代数構造に拡張したことが新しい。本結果はトップ国際会議である Logic in Computer Science に採録された。
(2) π計算のための交差型システムについては、前年度までに技術的な課題が明らかになっていた。本年度は、技術的困難の詳細な調査と解決を目指し、π計算の理論を代数的観点から見直す研究を行った。成果は国際会議 European Symposium on Programming に再録された。本結果が明らかにしたことは、π計算は線形論理という論理体系の特殊な形であると理解できるこいうことである。線形論理と交差型システムの関連は良く知られており、本結果はπ計算の交差型システムへの指針を与えることが期待できる。

  • 研究成果

    (3件)

すべて 2019 2018

すべて 雑誌論文 (3件) (うち国際共著 1件、 査読あり 2件)

  • [雑誌論文] A Categorical Model of an $$\mathbf {i/o}$$ -typed $$\pi $$ -calculus2019

    • 著者名/発表者名
      Sakayori Ken、Tsukada Takeshi
    • 雑誌名

      Proceedings of the 28th European Symposium on Programming

      巻: 0 ページ: 640~667

    • DOI

      10.1007/978-3-030-17184-1_23

  • [雑誌論文] Higher-Order Program Verification via HFL Model Checking2018

    • 著者名/発表者名
      Kobayashi Naoki、Tsukada Takeshi、Watanabe Keiichi
    • 雑誌名

      Proceedings of the 27th European Symposium on Programming

      巻: 0 ページ: 711~738

    • DOI

      10.1007/978-3-319-89884-1_25

    • 査読あり
  • [雑誌論文] Species, Profunctors and Taylor Expansion Weighted by SMCC2018

    • 著者名/発表者名
      Tsukada Takeshi、Asada Kazuyuki、Ong C.-H. Luke
    • 雑誌名

      Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

      巻: 0 ページ: 889-898

    • DOI

      10.1145/3209108.3209157

    • 査読あり / 国際共著

URL: 

公開日: 2019-12-27  

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

Powered by NII kakenhi