Dependent types are a feature of type theory and type systems used to encode logic's quantifiers. They enable the programmer to assign types that further restrain the set of possible implementations, reducing bugs. Examples include dependent functions and dependent pairs, where the return type or second value may depend on the value of an argument. Deciding type equality may involve deciding whether two arbitrary programs produce the same result.
Carnegie Mellon University
Spring 2014
A comprehensive course at Carnegie Mellon University that introduces fundamental principles of programming language design and implementation from a mathematical perspective. It delves deep into the structural and dynamic aspects of programming languages, studying concepts like recursion, objects, polymorphism, and parallelism.
No concepts data
+ 38 more concepts