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
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.
