❏証明論に基づくコンパイラの系統的な構築法の研究(22500023)
【研究テーマ】ソフトウエア
【研究種目】基盤研究(C)
【研究期間】2010 - 2012
【研究代表者】大堀 淳 東北大学, 電気通信研究所, 教授 (60252532)
【キーワード】コンパイラ / 証明論 / 最適化 / プログラミング言語処理系
【概要】本研究では,プログラミング言語のコンパイルの過程に現れる種々の中間言語は,直感主義的論理学の証明システムとして表現でき,それらの言語間の変換は,証明変換として表現できるはずである,との基本的な洞察を基礎とし,関数型言語のコンパイル過程を自然演繹システムから,コード言語を表現するある種のシーケント計算系にいたる証明変換の合成として表現でき,その変換可能性を示すメタレベルの証明から,コンパイルアルゴリ...