---
key: pl/coq
kind: plang
name: "Coq"
url: https://plangs.page/coq
---

# Coq

> Interactive theorem prover focused on formal verification and proof checking.

Interactive theorem prover that allows users to write formal mathematical definitions, executable algorithms, and theorems, mechanically check proofs of those properties, and extract a certified program from proofs. It leverages the calculus of inductive constructions for these purposes. Coq is widely utilized in formal verification projects and mathematical proof checking.

## Facts

- Appeared: 1989
- Homepage: https://coq.inria.fr/
- GitHub: https://github.com/coq/coq
- Languish ranking: #224

## Relationships

### Paradigms

- [Declarative](https://plangs.page/paradigm/declarative)
- [Functional](https://plangs.page/paradigm/functional)
- [Logic](https://plangs.page/paradigm/logic)

### Platforms

- [Cross-Platform](https://plangs.page/platform/cross)

### Type Systems

- [Dependent](https://plangs.page/type-system/dependent)
- [Static](https://plangs.page/type-system/static)
- [Strong](https://plangs.page/type-system/strong)

### Influenced By

- [OCaml](https://plangs.page/ocaml)

### Influenced

- [Agda](https://plangs.page/agda)
- [Idris](https://plangs.page/idris)

### Written With

- [OCaml](https://plangs.page/ocaml)

### Licenses

- [LGPL](https://plangs.page/license/lgpl)

### Tags

- [Educational](https://plangs.page/tag/edu)
- [Interpreter](https://plangs.page/tag/interpreters)
- [Proof Assistant](https://plangs.page/tag/proofs)