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

2017 年度 研究成果報告書

マルチステージ証明記述言語の設計と開発

研究課題

  • PDF
研究課題/領域番号 15K12007
研究種目

挑戦的萌芽研究

配分区分基金
研究分野 ソフトウェア
研究機関筑波大学

研究代表者

亀山 幸義  筑波大学, システム情報系, 教授 (10195000)

研究協力者 坂口 和彦  筑波大学, システム情報工学研究科
渡部 恭久  筑波大学, システム情報工学研究科
大石 純平  筑波大学, システム情報工学研究科
薄井 千春  筑波大学, システム情報工学研究科
須藤 悠斗  筑波大学, システム情報工学研究科
研究期間 (年度) 2015-04-01 – 2018-03-31
キーワード証明記述言語 / プログラム生成 / メタプログラミング / コントロールエフェクト / 副作用 / 型安全性 / モジュール
研究成果の概要

本研究はメタプログラミングの手法・研究成果を、定理証明系における証明記述言語に適用することを目的とした研究である。メタプログラミングの中でも静的な型付けによる安全性の保証を与える手法に基づいて、破壊的変数や限定継続などのコントロールオペレータを用いてコード生成器の記述言語の表現力を高めるとともに、生成されるコードの記述言語にモジュールを追加した場合の拡張についても考察し、いずれも健全性が成立し一定の記述力をもつ型システムの設計に成功した。これを用いて非常に簡単な証明記述言語を設計し、副作用を含む証明生成器を記述する手法にについての知見を得ることができた。

自由記述の分野

プログラミング言語論、関数プログラミングと方システム、プログラム生成、定理証明

URL: 

公開日: 2019-03-29  

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

Powered by NII kakenhi