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
|
| Project Status |
Completed (Fiscal Year 2012)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2012: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2011: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2010: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| 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.
|
Report
(4 results)
Research Products
(21 results)
