| 大会名称 |
|---|
| 2009年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2009 |
| 発行日 |
| 2009/8/20 |
| セッション番号 |
| 7A |
| セッション名 |
| プログラミング |
| 講演日 |
| 2009/09/04 |
| 講演場所(会議室等) |
| A会場（9号館1F 911教室） |
| 講演番号 |
| A-031 |
| タイトル |
| コンパイラ構築の証明論的枠組み |
| 著者名 |
| 大堀 淳, |
| キーワード |
| プログラミング言語, コンパイラ, 証明論 |
| 抄録 |
|
本講演では,直感主義的論理学の証明論を基礎とする新しいコンパイラ構築の 枠組みを提示する.この枠組みでは,コンパイルの各段階に現れる中間言語や ターゲット言語であるマシンコードはすべて,それぞれの計算の性質を反映し た証明システムとして表現され,コンパイルステップは,それら証明システム 間の証明変換として与えられる.この枠組みでは,型保存などのコンパイラの 正しに関する多くの性質が,複雑なメタレベルの性質を証明することなく,コ ンパイラの構成そのものから,直接帰結する.コンパイルは証明変換であるか ら定義上,コンパイルされたコードの型は存性される.コンパイルされたコー ドの意味の保存性は,各証明変換が,カット除去に関する性質を保存すること から帰結する. |
| 本文pdf |
| PDF download (52.2KB) |