The Rocq Prover is an interactive theorem prover first released in 1989. It allows the expression of mathematical assertions, mechanical checking of proofs of these assertions, assists in finding formal proofs using proof automation routines and extraction of a certified program from the constructive proof of its formal specification. Wikipedia

Created Year: 1984
Developed by: Institut National de Recherche en Informatique et en Automatique
Operating systems: cross-platform
Implemented in: C • OCaml
Named after: Roc, Rocquencourt, Thierry Coquand, stone

Wikidata: Q1131652

Influenced: Agda • Idris • Lean

Programming paradigms: purely functional programming

Language types: dependently typed programming language • purely functional programming language