Translation from Classical to Intuitionistic Logic

2015 Fiscal Year Final Research Report

• 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
• Keywords: 古典論理 / 直観主義論理 / 簡約保存 / CPS変換 / 強正規化性

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.

Free Research Field

計算系の論理学的基礎理論