Dependent types

From The Twelf Project
(Redirected from Dependent type)
Jump to: navigation, search

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

This page is incomplete. We should expand it.