Saltar para o conteúdo

Coq

Origem: Wikipédia, a enciclopédia livre.

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

  1. Bertot e Castéran, 2004, pp. 1-5.
  2. Bertot e Castéran, 2004, pp. 187-210.
  3. The Coq Proof Assistant. What is Coq?. Acesso em: 02 dez. 2018
  4. OCaml. Success Stories. Acesso em: 02 dez. 2018
  5. The Coq Proof Assistant. Coq 8.8.2 is out. Acesso em: 02 dez. 2018
  6. ACM SIGPLAN. Programming Languages Software Award. Acesso em: 02 dez. 2018.
  7. Dopplick, Renee. Open Source Coq Wins ACM Software System Award. Acesso em: 02 dez. 2018.
  • 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.

Ligações externas

[editar | editar código-fonte]