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.