Dependent types
From The Twelf Project
A language with dependent types has types which can mention the terms they classify. For example, LF is a dependently typed language because LF types can mention LF terms.
See also
- LF
- Dependent types at Wikipedia
- Chapter 2 of Advanced Topics in Types and Programming Languages
This page is incomplete. We should expand it.
