Classical logic and infinite phenomena in computation
| 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
|
| 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)
Research Products
(7 results)
-
-
[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
Int'l Joint Research
-
-
-
-
-
