Translation from Classical to Intuitionistic Logic
| Project/Area Number |
24650002
|
|---|
| Research Category |
Grant-in-Aid for Challenging Exploratory Research
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
SAKURAI Takafumi 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
|
|---|
| Research Collaborator |
SATO Masahiko
KIKUCHI Kentaro
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
Fiscal Year 2014: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2013: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2012: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | 古典論理 / 直観主義論理 / 簡約保存 / CPS変換 / 強正規化性 / C(G)PS変換 / intersection-union / intersection-product / 表示的意味 |
|---|
| Outline of Final Research Achievements |
We present strict reduction-preserving translations from classical type systems to intuitionistic type systems. The classical type systems we consider are lambda-bar-mu, call-by-name lambda-bar-mu-tilde, call-by-value lambda-bar-mu-tilde and lambda-mu. The contributions of this research are the new translations and the systematic view of the various translations. To achieve these results, we introduce several simple translations and derive our new translations and the known translations by composing the simple translations. The immediate consequence of our translations is the strong normalization property of each type system.
|
Report
(5 results)
Research Products
(4 results)
