2009 Fiscal Year Self-evaluation Report

Type theory for permutative conversions

Research Project

Project/Area Number	19540156
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Single-year Grants
Section	一般
Research Field	General mathematics (including Probability theory/Statistical mathematics)
Research Institution	National Institute of Informatics
Principal Investigator	TATSUTA Makoto National Institute of Informatics, 情報学プリンシプル研究系, 教授 (80216994)
Project Period (FY)	2007 – 2010
Keywords	型理論 / 置換簡約
Research Abstract	置換簡約の強正規化可能性は近年活発に研究されている。また、定理自動証明システムCoqは、フランスで研究開発されている証明システムで、基本理論と応用の両面で成功している。本研究では、これらの研究成果を深化発展させることにより、置換簡約の型理論の研究を行う。