証明論に基づくコンパイラの系統的な構築法の研究
【研究分野】ソフトウエア
【研究キーワード】
コンパイラ / 証明論 / 最適化 / プログラミング言語処理系
【研究成果の概要】
本研究では,プログラミング言語のコンパイルの過程に現れる種々の中間言語は,直感主義的論理学の証明システムとして表現でき,それらの言語間の変換は,証明変換として表現できるはずである,との基本的な洞察を基礎とし,関数型言語のコンパイル過程を自然演繹システムから,コード言語を表現するある種のシーケント計算系にいたる証明変換の合成として表現でき,その変換可能性を示すメタレベルの証明から,コンパイルアルゴリズムが抽出できることを示した.
【研究代表者】
【研究分担者】 |
上野 雄大 | 東北大学 | 電気通信研究所 | 助教 | (Kakenデータベース) |
森畑 明昌 | 東北大学 | 電気通信研究所 | 助教 | (Kakenデータベース) |
|
【研究種目】基盤研究(C)
【研究期間】2010 - 2012
【配分額】3,770千円 (直接経費: 2,900千円、間接経費: 870千円)