---
key: tsys/dependent
kind: typeSystem
name: "Dependent"
url: https://plangs.page/type-system/dependent
---

# Dependent

Type system where types depend on terms, allowing for more expressive type constraints.

## Facts

- Homepage: https://en.wikipedia.org/wiki/Dependent_typing

## Relationships

### Plangs

- [Agda](https://plangs.page/agda)
- [Coq](https://plangs.page/coq)
- [Futhark](https://plangs.page/futhark)
- [Idris](https://plangs.page/idris)
- [Isabelle](https://plangs.page/isabelle)