Classical logic and infinite phenomena in computation

2017 Fiscal Year Final Research Report

• Project/Area Number: 15K00012
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Theory of informatics
• Research Institution: Nagoya University
• Principal Investigator: Nakazawa Koji 名古屋大学, 情報学研究科, 准教授 (80362581)
• Project Period (FY): 2015-04-01 – 2018-03-31
• 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.

Free Research Field

プログラミング言語，数理論理学