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

Classical logic and infinite phenomena in computation

Research Project

Project/Area Number 15K00012
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Theory of informatics
Research InstitutionNagoya University

Principal Investigator

Nakazawa Koji  名古屋大学, 情報学研究科, 准教授 (80362581)

Project Period (FY) 2015-04-01 – 2018-03-31
Project Status Completed (Fiscal Year 2017)
Budget Amount *help
¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2016: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2015: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Keywordsラムダ計算 / 古典論理 / 合流性 / ラムダ・ミュー計算 / カット除去 / 交叉型
Outline of Final Research Achievements

The results of this project are the following: (1) We study some fundamental properties of the Lambda-mu calculus, which is a computational model of programming language with stream data. In particular, We propose a new proof technique, called the compositional Z theorem, to prove confluence of the calculus. (2) We show that the compositional Z theorem can be widely applied to prove confluence of several calculi with permutation-like reduction, such as the lambda calculus with direct sum, the lambda calculus with explicit substitutions, and the call-by-value lambda calculus with permutation rules. (3) We propose an intersection-type system for a calculus corresponding to the classical sequent calculus, which reflects the symmetry of classical logic. We show that the system is complete and can characterize the strong normalization.

Report

(4 results)
  • 2017 Annual Research Report   Final Research Report ( PDF )
  • 2016 Research-status Report
  • 2015 Research-status Report
  • Research Products

    (7 results)

All 2017 2016 2015

All Journal Article (1 results) (of which Peer Reviewed: 1 results,  Acknowledgement Compliant: 1 results) Presentation (6 results) (of which Int'l Joint Research: 3 results,  Invited: 1 results)

  • [Journal Article] Compositional Z: Confluence proofs for permutative conversion2016

    • Author(s)
      Koji Nakazawa and Ken-etsu Fujita
    • Journal Title

      Studia Logica

      Volume: 104 Issue: 6 Pages: 1205-1224

    • DOI

      10.1007/s11225-016-9673-0

    • NAID

      120005971246

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Acknowledgement Compliant
  • [Presentation] Z for call-by-value2017

    • Author(s)
      Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa
    • Organizer
      6th International Workshop on Cofluence (IWC 2017)
    • Related Report
      2017 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Church-Rosser theorem and compositional Z-property2016

    • Author(s)
      Ken-etsu Fujita and Koji Nakazawa
    • Organizer
      日本ソフトウェア科学会第33回大会
    • Place of Presentation
      東北大学
    • Year and Date
      2016-09-06
    • Related Report
      2016 Research-status Report
  • [Presentation] Intersection and Union Type Assignment and Polarised lambda-bar-mu-mu-tilde2016

    • Author(s)
      Takeshi Tsukada and Koji Nakazawa
    • Organizer
      第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)
    • Place of Presentation
      岡山
    • Year and Date
      2016-03-08
    • Related Report
      2015 Research-status Report
  • [Presentation] Characterizing trees for lambda-mu terms2016

    • Author(s)
      Koji Nakazawa
    • Organizer
      8th International Workshop on Higher-Order Rewriting (HOR 2016)
    • Place of Presentation
      ポルト,ポルトガル
    • Related Report
      2016 Research-status Report
    • Int'l Joint Research
  • [Presentation] Compositional Z: Confluence Proofs for Permutative Conversion2015

    • Author(s)
      Koji Nakazawa and Ken-etsu Fujita
    • Organizer
      第32回日本ソフトウェア科学会大会
    • Place of Presentation
      東京
    • Year and Date
      2015-09-10
    • Related Report
      2015 Research-status Report
  • [Presentation] Lambda Calculi and Confluence from A to Z2015

    • Author(s)
      Koji Nakazawa
    • Organizer
      4th International Workshop on Confluence (IWC2015)
    • Place of Presentation
      Berlin
    • Year and Date
      2015-08-02
    • Related Report
      2015 Research-status Report
    • Int'l Joint Research / Invited

URL: 

Published: 2015-04-16   Modified: 2019-03-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi