Type Theory of Existential Types

2014 Fiscal Year Final Research Report

• Project/Area Number: 23500030
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Fundamental theory of informatics
• Research Institution: National Institute of Informatics
• Principal Investigator: TATSUTA Makoto 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
• Co-Investigator(Renkei-kenkyūsha): NAKAZAWA Koji 京都大学, 情報学研究科, 助教 (80362581)
• Project Period (FY): 2011-04-28 – 2015-03-31
• Keywords: 型理論 / 存在型

Outline of Final Research Achievements

(1) Bimorphic recursion is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. We showed bimorphic recursion has principal types and decidable type inference. (2) We extended the dual calculus with inductive types and coinductive types. We first introduced a non-deterministic dual calculus with inductive and coinductive types, and proved its strong normalization. Next we introduced a call-by-value system and a call-by-name system of the dual calculus with inductive and coinductive types, and showed their Church-Rosser property, and their strong normalization. (3) This paper proposes games with Sequential Backtracking, and proves that they provide a sound and complete semantics for subclassical logics.

Free Research Field

プログラム理論