Pinned Repositories
atbr-plugin
coq
Coq with extensions for proof engineering
coq-ast
Coq plugin for printing term abstract syntax trees and their digests
coq-docker
Dockerfiles with various versions of Coq
coqhammer
A fork of the CoqHammer proof automation plugin
proofengineering-bib
BibTeX bibliographies for proof engineering-related papers
proofengineering-doc
Documentation related to proof engineering
proofengineering.github.io
Studying Software Engineering in the Proof Assistant world.
regmatch
Certified regular expression matcher in Coq
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
ProofEngineering's Repositories
proofengineering/proofengineering-bib
BibTeX bibliographies for proof engineering-related papers
proofengineering/coq-ast
Coq plugin for printing term abstract syntax trees and their digests
proofengineering/proofengineering.github.io
Studying Software Engineering in the Proof Assistant world.
proofengineering/proofengineering-doc
Documentation related to proof engineering
proofengineering/regmatch
Certified regular expression matcher in Coq
proofengineering/coq
Coq with extensions for proof engineering
proofengineering/coq-docker
Dockerfiles with various versions of Coq
proofengineering/coqhammer
A fork of the CoqHammer proof automation plugin
proofengineering/atbr-plugin
proofengineering/coqproject-legacy
proofengineering/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
proofengineering/coq-depends
Coq plugin for plain dependency extraction
proofengineering/coq-dpdgraph
Build dependency graphs between COQ objects
proofengineering/htt
Hoare Type Theory
proofengineering/icoq
A regression proof selection tool for the Coq proof assistant
proofengineering/opam-repository
Proof engineering released package repository for OPAM
proofengineering/opam-repository-dev
Proof engineering development package repository for OPAM
proofengineering/ott
Ott is a tool for writing definitions of programming languages and calculi
proofengineering/reglang
OPAM friendly version of files from the paper Regular Language Representations in the Constructive Type Theory of Coq
proofengineering/serapi-tests
Some Coq regression tests for SerAPI