内类型理论

Many open problems in type theory can be described in terms of internal definability. What internal definability deals with is type theory within type theory. We call internal type theory the one that studies type theory or encoding within type theory. From the point of view of category theory, a type system corresponds to a category or a fibration and an internal type system corresponds to an internal category or small fibration. Internal categories and small fibrations play very important roles in category theory and the theory of fibraiton. It is reasonable to expect that internal category theory should also play an equally important role in type theory. The present project has examined these basic problems in internal type theory. The main achievements of the project are:.(1) Characterization of properties of internal type systems in terms of internal logic. The general idea is similar to that of Calculus of Constructions. An internal logic is introduced in logical framework to describe internal properties of internal type systems. Our result shows that the relationship between a logical framework and encoding within the framework is the same as that between a category and internal category defined within the category.(2) Semantic models of internal type systems. The key result is a generalization of the fibration models so that they are equipped with a notion of internal equality. This internal equality is used to model definitional equalities of internal type systems. (3) Internal definability between polymorphic lambda calculi. The main result is that the n-th order polymorhic lambda calculus is internally definable in the (n+1)-th order polymorphic lambda calculus.Under the support of this project, we have also organized three workshops: BASICS'00, BASICS02 and APLAS'02.

在申请人提出的逻辑框架的内可定义性基础上提出并研究内容型理论。主要研究内容包括：内容型理论的元性质、高阶多态演算的内可定义性、内容型理论的内逻辑刻划、内容型理鄣挠镆迥Ｐ汀１旧昵胂钅康难芯慷缘バ吐矶∨捣蚶嘈屠砺墼灾实难芯坑兄匾羰隆⒂兄诖由畈愦紊侠斫饫嘈屠砺壑械囊恍┮赡盐侍狻