Dependent type system with subtyping (I) type level transitivity elimination
Dependent Type System with Subtyping (I)Type Level Transitivity Elimination

Dependent type systems are the basis of many proof development environments. In Aspinall and Compagnoni's paper, a system λP ≤ is proposed as a subtyping extension of the first order dependent type system λP (also called λΠ). λP ≤, has nice meta-theoretic properties including subject reduction and decidability. In this article, we give a reformulation of λP ≤, called λΠ≤. The advantages of λΠ≤ include: type level transitivity elimination property and pretype-based subtyping system. These features considerably facilitate the meta-theoretical study and further extensions of this system. This work is supported by Programme PRA M4, Association Franco-Chinoise pour la Recherche Scientifique et Technique, and Bourse du Ministère des Affaires Etrangères du Gouvernment Fran?ais. Due to the limitation of the pages of the journal, this paper has been splited into two parts. This is the first part of the paper. The second part will appear on Vol. 14, No. 2 or No.3 of this journal. Chen Gang received the B.S. degree from Department of Mathematics, Zhejiang University; the M.S. degree from Department of Computer Science, Peking University. He is presently a Ph.D. candidate in computer science at University Paris 7 and Ecole Normale Supérieure, Paris. His research interests include type theory, subtyping, proof assistant, object-oriented programming language and artificial intelligence.