Semantics of Intensional Type Theory extended with Decidable Equational Theories

摘要

Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions (CC) provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensional