Dependent type

[Google Scholar] [Wikipedia]

Notes: Lean theorem prover, Coq theorem prover, ASL, Sail language, type inference, liquid type

A dependent type is a type whose definition depends on a value.

Some common forms of dependent type are

  • product types Π
  • sum types Σ
  • sized vector types such as “N-bit bitvectors”.

See also: Barendregt cube.


Arm Architecture Specification Language (ASL), Coq theorem prover, Liquid type, Phantom types, Sail ISA specification language