Skip to content
◈ALB Atlas

Rocq Alive

Rocq
KindProgramming language
Appeared1989
StatusAlive
CreatorThierry Coquand / INRIA
FamilyML
Also known asCoq
Sourcerocq-prover.org ↗

Calculus of Constructions made usable — the proof assistant behind CompCert and the four-color theorem's machine-checked proof; renamed Rocq in 2024.

Created by Thierry Coquand

INRIA's Coq (1989) — the Calculus of Inductive Constructions — is the proof assistant: programs and proofs in the same language, extraction to OCaml/Haskell, and the CompCert verified C compiler built in it.\n\nRenamed Rocq in 2024; it is where mathematics and code formally meet.

Timeline

2024Renamed from Coq to Rocq

Sources

  1. rocq-prover.org/
  2. en.wikipedia.org/wiki/Coq_(software)