Bibliotecas escritas em Coq
stalin-sort
Adicione um algoritmo stalin sort em qualquer idioma que você goste ❣️ se quiser, dê-nos um ⭐️.
- 1.2k
- MIT
Coq-HoTT
Uma biblioteca Coq para a Teoria dos Tipos de Homotopia.
- 1.2k
- GNU General Public License v3.0
UniMath
Esta biblioteca coq visa formalizar um corpo substancial de matemática usando o ponto de vista univalente.
- 853
- GNU General Public License v3.0
magmide
Uma linguagem de prova de tipagem dependente destinada a tornar o código bare metal comprovadamente correto possível para engenheiros de software.
- 771
CoqGym
Um ambiente de aprendizagem para demonstração de teoremas com o assistente de prova Coq.
- 332
- GNU Lesser General Public License v3.0 only
proofs
Meu repositório pessoal de matemática formalmente verificada.
- 259
- GNU General Public License v3.0
Coq-Equations
Um pacote de definição de função para Coq.
- 197
- GNU Lesser General Public License v3.0 only
verdi-raft
Uma implementação do protocolo de consenso distribuído Raft, verificado em Coq usando a estrutura Verdi.
- 168
- BSD 2-clause "Simplified"
analysis
Biblioteca de análise compatível com componentes matemáticos (por math-comp).
- 158
- GNU General Public License v3.0
fiat
Síntese principalmente automatizada de programas corretos por construção.
- 140
- GNU General Public License v3.0
kami
Uma plataforma para especificação de hardware paramétrico de alto nível e sua verificação modular (por mit-plv).
- 126
- MIT
toychain
Um consenso blockchain minimalista implementado e verificado no Coq.
- 106
- BSD 2-clause "Simplified"
koika
Uma linguagem central para design de hardware baseado em regras 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
Especificação formal e verificação de hardware, especialmente para segurança e privacidade.
- 97
- Apache License 2.0
coq-library-undecidability
Uma biblioteca de provas de indecidibilidade mecanizadas no assistente de prova Coq.
- 96
- GNU General Public License v3.0
vericert
Uma ferramenta de síntese de alto nível formalmente verificada baseada em CompCert e escrita em Coq..
- 71
- GNU General Public License v3.0 only
scala-escape
Um plug-in de compilador para controlar o tempo de vida do objeto em Scala (por TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"