Injective pure type systems form a large class of pure type systems for which one can compute by purely syntactic means two sorts elmt(Γ/M) and sort(Γ/M), where Γ is a pseudo-context and M is a pseudo-term we provide a sound and complete type-checking algorithm for injective pure type systems. In addition, we prove expansion postponement for a variant of injective pure type systems where the problematic clause in the (abstraction) rule is replaced In favor of constraints over elmt(.l.) and sort(.1.).
展开▼
