Types with extra structure: predicates, equations, composition - Hewer, Brandon (2024)
Intuitionistic type theory was first introduced by Martin-Lof [1984] as a foundation for constructive mathematics and also serves as a dependently typed programming language. Dependent types provide us with a framework to reason about and guide the construction of programs by specifying both their structure and properties in a manner that can be automatically verified by a type-checker.