扩展语义数据类型

The research on theoretical computer science spurs directly the development of programming technologies, programming languages and their semantics, for which λ-calculus and type theory are ideal research tools. The project aimed at extending the usual concept of semantic data type such that the extended notion would characterize the intuitive meaning of data type and cover more formulae in second order logic. One result of the project is the decidability of positive types in System F in the sense of global constructive provability, which is the usual inhabitation problem in second order typed λ-calculi in a strong sense. Under Curry-Haward correspondence, this means a characterization on all proofs of the corresponding theorems. Moreover, we established an intuitionistic inference system by working with Prof. G. Dowek (France), and proved its soundness and completeness. We developed in this way a method for proving that inhabitation problem is decidable for positive types. This method can be applied to the positive fragment of System F, higher-order logic, and automatic reasoning. Another result of the project is a study on a problem of largest Cartesian closed category in the setting of stable domains, working with Prof. Zhang Guo-Qiang (U.S.A.). This is an open problem of R. Amadio and P.-L. Curien dated back to early 90th. The resolving of this problem will be helpful to the denotational semantics of programming languages. We have also obtained some important results on the self-reduction in λ-calculus.

该项目源于法国J.L.Krivine教授的一个猜想，拟对J.Y.Girard教授（线形逻辑的创始人）腇系统的某些类型中任意给定类型的全体可类化项予以刻画；即，在Curry-Haward的对应下，对其相应定理的全体证明给予刻画。进而建立一个扩展语义数据类的概念。