Coq
Na ciência da computação, Coq é 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. Coq trabalha dentro da teoria do cálculo de construções indutivas, derivada do cálculo de construções.[1] Coq 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.[2]
Coq é um software livre e de código aberto, licenciado sob a licença GNU Lesser General Public License Version 2.1.[3] É escrito majoritariamente na linguagem de programação OCaml.[4] A versão 8.8.2 foi lançada em 26 de setembro de 2018.[5]
Coq foi laureado com os prestigiosos prêmios ACM SIGPLAN Programming Languages Sofware Award, em 2013, e ACM Software System Award, em 2014.[6][7]
Referências
- ↑ 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[editar | editar código-fonte]
- 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.