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

2013 年度 実施状況報告書

依存型理論による安全性保証付きデータ構造の創出・推論・進化

研究課題

研究課題/領域番号 24300001
研究機関群馬大学

研究代表者

浜名 誠  群馬大学, 理工学研究科, 助教 (90334135)

研究期間 (年度) 2012-04-01 – 2015-03-31
キーワードプログラム理論 / 代数理論 / 依存型 / データ構造 / 情報学基礎 / プログラム意味論 / 多相型
研究概要

本年度は、依存型を形式的に論じるためのモデルの等式論理の確立を行った。結果、様々な多相システムを統一的に扱うための体系である多相型代数理論を構築することに成功した。一般化依存多項式を用いることで、任意のシグネチャによる多相型構文と項中の型の代入を厳密にモデル化することができた。そして代数的モデルを持つ論理体系を圏論的考察から導出し、その正当性を証明した。特に多相型の型宇宙はΣモノイドであることを明らかにし、これにより複数の型宇宙の間の変換を議論することが可能となった。これにより既存の種々の型理論とモデルを統一、単純化し、その本質を明確化する理論となった。また、この体系が確かに様々な実際例を統一的に扱うことができることを実際に例示することにより示した。これをまとめた論文は、理論計算機科学のトップ国際会議 ACM/IEEE Logic in Computer Science (LICS'13)に採択され、IEEE Pressから出版された。

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

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

理由

おおむね順調に進展している。
型の進化を議論するためのフレームワークとして、等しい対象を論ずるための論理、等式論理として多相型等式理論を構築できた。

今後の研究の推進方策

本年度は、The European Joint Conferences on Theory and Practice of Software (ETAPS)併設の国際ワークショップMathematically Structured Functional Programming 2014のプログラム委員、および国内最大のプログラミング言語会議PPLのプログラム委員を務め、型理論および関数型プログラミングの最新進展状況を把握し、関連研究者から有用な研究推進の情報を得た。今後はこれらも参考にし、依存型の計算機構の研究を進める。

次年度の研究費の使用計画

前倒し申請をした分が、その後の研究の進行が当初どおりだったため実際は使用しなかった。
当初の予定通りに使用する。

  • 研究成果

    (6件)

すべて 2013 その他

すべて 雑誌論文 (1件) (うち査読あり 1件) 学会発表 (5件)

  • [雑誌論文] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic2013

    • 著者名/発表者名
      M. Fiore and M. Hamana
    • 雑誌名

      Proc. of Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)

      巻: 2013 ページ: 520-529

    • DOI

      http://doi.ieeecomputersociety.org/10.1109/LICS.2013.59

    • 査読あり
  • [学会発表] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic

    • 著者名/発表者名
      Makoto Hamana
    • 学会等名
      Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'13)
    • 発表場所
      New Orleans, USA
  • [学会発表] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic

    • 著者名/発表者名
      Makoto Hamana
    • 学会等名
      Category Theory Conference (CT'13)
    • 発表場所
      Macquarie University, Sydney, Australia
  • [学会発表] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic

    • 著者名/発表者名
      Makoto Hamana
    • 学会等名
      General Algebra and Its Applications (GAIA'13)
    • 発表場所
      La Trobe University, Melbourne, Australia
  • [学会発表] 多元宇宙多相型代数理論

    • 著者名/発表者名
      浜名誠
    • 学会等名
      日本ソフトウェア科学会第30回大会
    • 発表場所
      東京大学
  • [学会発表] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic

    • 著者名/発表者名
      Makoto Hamana
    • 学会等名
      NII Shoan Workshop on Coinduction for computation structures and programming languages
    • 発表場所
      湘南国際村

URL: 

公開日: 2015-05-28  

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

Powered by NII kakenhi