About The Rocq Prover

The Rocq Prover implements a high-level program specification and mathematical language called Gallina that is based on an expressive formal language called the Polymorphic, Cumulative Calculus of Inductive Constructions that itself combines both a higher-order logic and a richly-typed functional programming language. Through a vernacular language of commands, the Rocq Prover allows:

• to define data structures, functions or predicates, that can be evaluated efficiently;
• to state mathematical theorems and software specifications;
• to interactively develop formal proofs of these theorems;
• to machine-check these proofs by a relatively small certification "kernel";
• to extract certified programs to languages like OCaml, Haskell or Scheme.

As a proof development system, the Rocq Prover provides interactive proof methods, decision and semi-decision algorithms, and a tactic language for letting the user define its own proof methods. Connection with external computer algebra systems or theorem provers is available.

As a platform for the formalization of mathematics or the development of programs, the Rocq Prover provides support for high-level notations, implicit contents and other mechanisms for formalization at scale.

Read more about the features that make the Rocq Prover unique in the Why Rocq? section.

A Brief History

The Rocq Prover is the result of more than 40 years of research. It started in 1984 from an implementation of the Calculus of Constructions at INRIA-Rocquencourt by Thierry Coquand and Gérard Huet. In 1991, Christine Paulin extended it to the Calculus of Inductive Constructions. All in all, more than 200 people have contributed to the development of Rocq.

The Rocq Team is responsible for the development of Rocq and integration of contributions. See the changelog for a detailed list of contributors in each release of Rocq and the history page in the reference manual for the early history of Rocq.

The Rocq Prover is written in OCaml. It is distributed under the GNU Lesser General Public Licence Version 2.1 (LGPL).

An Overview of the Name's Evolution

The Rocq Prover was formerly known as the Coq Proof Assistant. The name "Coq" referenced the Calculus of Constructions (CoC), the foundational system it is based on, as well as one of its creators, Thierry Coquand. Additionally, it paid homage to the French national symbol, the rooster.

The new name, "the Rocq Prover", honors Inria Rocquencourt, the original site where the prover was developed. It also alludes to the mythological bird Roc (or Rokh), symbolizing strength and not so disconnected to a rooster. Furthermore, the name conveys a sense of solidity, and its unintended connection to music adds a pleasant resonance. The new name was chosen by the Core team after a poll of the users, see this page for a detailed breakdown of the results.