Dependently Typed Proof Assistant Languages

Dependently Typed Proof Assistant Languages are functional programming languages whose type systems allow a type to depend on a value, letting a program's own type checker verify logical proofs as well as ordinary code. The Wikipedia article on the dependent type names Agda, Rocq (previously known as Coq), Idris and Lean together as functional programming languages that use dependent types to help reduce bugs, grouping them as a real, attested class rather than a loose resemblance. Coq, now developed under the name Rocq, and Lean are both widely used as interactive proof assistants for formalizing mathematics, while Agda and Idris are general-purpose dependently typed languages that are also used for proof work. Each member placed under this group carries its own separate citation for the specific fact that places it in this family.