2012 Fiscal Year Final Research Report
A Study on Proof-Theoretical Foundations for Compiler Construction
| Project/Area Number |
22500023
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
OHORI Atsushi 東北大学, 電気通信研究所, 教授 (60252532)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
UENO Katsuhiro 東北大学, 電気通信研究所, 助教 (60551554)
MORIHATA Akimasa 東北大学, 電気通信研究所, 助教 (10582257)
|
|---|
| Project Period (FY) |
2010 – 2012
|
| Keywords | コンパイラ / 証明論 / 最適化 / プログラミング言語処理系 |
|---|
| Research Abstract |
Based on the novel observations that each of compiler intermediate languages can be represented as a proof system of the intuitionistic propositional logic, and that transformation between these languages corresponds to proof transformation, this research has shown that a compilation process of a functional language is represented by the composition of proof transformations from the natural deduction proof system to a variant of a sequent calculus that represents a code language, and that a compilation algorithm is mechanically extracted from the meta-level proof of the existence of such a proof transformation.
|
