2011 Fiscal Year Final Research Report

Calculi with Second-Order Existential Quantifier

Research Project

Project/Area Number	21700013
Research Category	Grant-in-Aid for Young Scientists (B)
Allocation Type	Single-year Grants
Research Field	Fundamental theory of informatics
Research Institution	Kyoto University
Principal Investigator	NAKAZAWA Koji 京都大学, 大学院・情報学研究科, 助教 (80362581)
Project Period (FY)	2009 – 2011
Keywords	型理論 / ラムダ計算 / 存在型 / 型検査 / 決定可能性
Research Abstract	We have got the following results on some type-related decision problems of calculi with second-order existential types :(1) for some typed lambda calculi where programs contain only partial type information, we have proved that type-checking and typability problems on polymorphic types are Turing reducible to those on existential types, and we have shown that those problems on existential types are undecidable,(2) we have proved the Turing equivalence between type-checking and typability problems in some fragments with existential type, and we have got new proofs of undecidability of typability in the domain-free lambda calculi with existential types, and(3) we have proved the Turing equivalence between the type-related problems in domain-free calculi with existential types and those in domain-free calculi with polymorphic types.

(5 results)