Coq
Na ciência da computação, Rocq (anteriormente conhecido como Coq[1]) é provador de teoremas interativo. Ele permite a expressão de asserções matemáticas, verifica mecanicamente as provas destas asserções, auxilia a encontrar provas formais e extrai um programa certificado a partir da prova construtiva de sua especificação formal. Rocq trabalha dentro da teoria do cálculo de construções indutivas, derivada do cálculo de construções.[2] Rocq não é um provador de teoremas automatizado, mas inclui táticas automáticas de demonstração de teoremas e vários procedimentos de decisão.[3]
Rocq é um software livre e de código aberto, licenciado sob a licença GNU Lesser General Public License Version 2.1.[4] É escrito majoritariamente na linguagem de programação OCaml.[5] A versão 8.8.2 foi lançada em 26 de setembro de 2018.[6]
Rocq foi laureado com os prestigiosos prêmios ACM SIGPLAN Programming Languages Sofware Award, em 2013, e ACM Software System Award, em 2014.[7][8]
Referências
- ↑ rocq-prover. «Alternative names». GitHub (em inglês). Consultado em 8 de dezembro de 2025
- ↑ Bertot e Castéran, 2004, pp. 1-5.
- ↑ Bertot e Castéran, 2004, pp. 187-210.
- ↑ The Coq Proof Assistant. What is Coq?. Acesso em: 02 dez. 2018
- ↑ OCaml. Success Stories. Acesso em: 02 dez. 2018
- ↑ The Coq Proof Assistant. Coq 8.8.2 is out. Acesso em: 02 dez. 2018
- ↑ ACM SIGPLAN. Programming Languages Software Award. Acesso em: 02 dez. 2018.
- ↑ Dopplick, Renee. Open Source Coq Wins ACM Software System Award. Acesso em: 02 dez. 2018.
Bibliografia
- Bertot, Yves; Castéran, Pierre. Interactive Theorem Proving and Program Development. Springer, 2004.
- Chlipala, Adam. Certified Programming with Dependent Types. MIT Press, 2004.
- Pierce, Benjamin et al. Software Foundations. Vol. 1: Logical Foundations. Acesso em: 02 dez. 2018.