証明論に基づくコンパイラの系統的な構築法の研究

2012 年度 研究成果報告書

• 研究課題/領域番号: 22500023
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 東北大学
• 研究代表者: 大堀 淳 東北大学, 電気通信研究所, 教授 (60252532)
• 研究分担者: 上野 雄大 東北大学, 電気通信研究所, 助教 (60551554) ; 森畑 明昌 東北大学, 電気通信研究所, 助教 (10582257)
• 研究期間 (年度): 2010 – 2012
• キーワード: コンパイラ / 証明論 / 最適化 / プログラミング言語処理系

研究概要

本研究では,プログラミング言語のコンパイルの過程に現れる種々の中間言語は,直感主義的論理学の証明システムとして表現でき,それらの言語間の変換は,証明変換として表現できるはずである,との基本的な洞察を基礎とし,関数型言語のコンパイル過程を自然演繹システムから,コード言語を表現するある種のシーケント計算系にいたる証明変換の合成として表現でき,その変換可能性を示すメタレベルの証明から,コンパイルアルゴリズムが抽出できることを示した.

研究成果

• [雑誌論文] SML#へのC言語の埋め込み (2012)
  • 著者名/発表者名: 篠埜功,大堀淳
  • 雑誌名: コンピュータソフトウェア 巻: Vol.29(2) ページ: 193-203
  • DOI: DOI:10.11309/jssst.29.2_193
  • 査読あり
• [雑誌論文] 多相レコード計算に基づく軽量な第一級オーバーロードの設計と実装 (2012)
  • 著者名/発表者名: 上野雄大,大堀淳
  • 雑誌名: コンピュータソフトウェア 巻: 29(1) ページ: 191-210
  • DOI: DOI:10.11309/jssst.29.1_191
  • 査読あり
• [学会発表] SML#のデータベース連携機能を活用したウェブアプリケーション構築技術 (2013)
  • 著者名/発表者名: 藤井貴啓,上野雄大,森畑明昌,大堀淳
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 福島県会津若松市
  • 年月日: 2013-03-05
• [学会発表] Rubyの操作的意味論の形式的定義に向けて (2013)
  • 著者名/発表者名: 深澤優鷹,上野雄大,森畑明昌,大堀淳
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ(ポスターセッション)
  • 発表場所: 福島県会津若松市
  • 年月日: 2013-03-05
• [学会発表] SML#のSQL統合へのgroupbyの導入 (2013)
  • 著者名/発表者名: 斎藤皓,上野雄大,森畑明昌,大堀淳
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ(ポスターセッション)
  • 発表場所: 福島県会津若松市
  • 年月日: 2013-03-05
• [学会発表] 二次元最大重み和問題のプログラム変換に基づく解法 (2013)
  • 著者名/発表者名: 小石真人,森畑明昌,大堀淳
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 福島県会津若松市
  • 年月日: 2013-03-04
• [学会発表] Making standard ML a practical database programming language (2011)
  • 著者名/発表者名: Atsushi Ohori, Katsuhiro Ueno
  • 学会等名: Proceedings of ACM International Conference of Functional Programming
  • 発表場所: Tokyo, Japan
  • 年月日: 2011-09-21
• [学会発表] Development of SML# - making ML an ordinary practical language (invited talk) (2011)
  • 著者名/発表者名: Atsushi Ohori
  • 学会等名: ACM ML Workshop
  • 発表場所: Tokyo, Japan
  • 年月日: 2011-09-18
• [学会発表] 宣言的記述からの関数型言語によるゲームプログラムの導出 (2011)
  • 著者名/発表者名: 松島勇介,上野雄大,森畑明昌,大堀淳
  • 学会等名: 第13回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 北海道札幌市(本発表は、学生の部発表賞を受賞)
  • 年月日: 2011-03-10
• [学会発表] 生存区間を変数名とする中間表現の実装と,それに基づく最適化 (2011)
  • 著者名/発表者名: 高橋和将,森畑明昌,上野雄大,大堀淳
  • 学会等名: 第13回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 北海道札幌市
  • 年月日: 2011-03-09