• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Translation from Classical to Intuitionistic Logic

Research Project

Project/Area Number 24650002
Research Category

Grant-in-Aid for Challenging Exploratory Research

Allocation TypeMulti-year Fund
Research Field Fundamental theory of informatics
Research InstitutionChiba 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)
  • 2015 Annual Research Report   Final Research Report ( PDF )
  • 2014 Research-status Report
  • 2013 Research-status Report
  • 2012 Research-status Report
  • Research Products

    (4 results)

All 2014 2013

All Journal Article (2 results) (of which Peer Reviewed: 2 results,  Acknowledgement Compliant: 1 results) Presentation (2 results)

  • [Journal Article] A Translation of Intersection and Union Types for the λμ-Calculus2014

    • Author(s)
      K. Kikuchi, T. Sakurai
    • Journal Title

      Lecture Note in Computer Science (Proceedings of 12th Asian Symposium on Programming Languages and Systems)

      Volume: LNCS 8858 Pages: 120-139

    • DOI

      10.1007/978-3-319-12736-1_7

    • ISBN
      9783319127354, 9783319127361
    • Related Report
      2014 Research-status Report
    • Peer Reviewed / Acknowledgement Compliant
  • [Journal Article] Viewing λ-terms through Maps2013

    • Author(s)
      M. Sato, R. Pollack, H. Schwichtenberg, T. Sakurai
    • Journal Title

      Indagationes Mathematicae

      Volume: 24 Issue: 4 Pages: 1073-1104

    • DOI

      10.1016/j.indag.2013.08.003

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Presentation] A Translation of Intersection and Union Types for the λμ-Calculus2014

    • Author(s)
      K. Kikuchi, T. Sakurai
    • Organizer
      Fifth International Workshop on Classical Logic and Computation (CL&C'14)
    • Place of Presentation
      Vienna, Austria
    • Year and Date
      2014-07-13
    • Related Report
      2014 Research-status Report
  • [Presentation] Viewing λ-terms through Maps2013

    • Author(s)
      M. Sato, R. Pollack, H. Schwichtenberg, T. Sakurai
    • Organizer
      TYPES Meeting 2013
    • Place of Presentation
      Toulouse, France
    • Related Report
      2013 Research-status Report

URL: 

Published: 2013-05-31   Modified: 2019-07-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi