Coq

O Rocq Prover (anteriormente chamado de Coq) é um provador de teoremas interativo lançado pela primeira vez em 1989. Ele permite a expressão de afirmações matemáticas, a verificação mecânica de provas dessas afirmações, auxilia na localização de provas formais usando rotinas de automação de prova e na extração de um programa certificado a partir da prova construtiva de sua especificação formal. Rocq trabalha dentro da teoria do cálculo das construções indutivas, uma derivada do cálculo das construções. Rocq não é um provador automatizado de teoremas, mas inclui táticas de automação de prova (procedimentos) e vários procedimentos de decisão. A Association for Computing Machinery concedeu a Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot e Pierre Castéran o ACM Software System Award de 2013 pelo Rocq (quando ainda era chamado de Coq).