Advances in Programming Languages 2018/19
Lecture 7
Dependent Types
This lecture completes the quartet of type/term interactions: after first-class functions, parameterized types, and polymorphic terms, we have types that depend on the value of terms. Example applications included types capturing vector lengths and matrix dimensions, as well as deep embedding for domain-specific languages and correctness of mathematical proofs.
- Tags
-