libcoq-stdlib

proof assistant for higher-order logic (theories)

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

coq-dpdgraph-tools

Coq plugin to extract dependencies between Coq objects (tools)

This package provides a plugin for Coq to extract dependencies between Coq objects and produce files with dependency information.

libcoq-equations

Coq library to work with functions defined by equations

This library provides a notation to write programs using dependent pattern-matching and well-founded recursion in Coq.

libcoq-hott

Coq library for homotopy type theory

This library is a formalization of homotopy type theory for Coq, where propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence.

libcoq-serapi-ocaml

interaction with Coq (runtime)

SerAPI provides a library for machine-to-machine interaction with Coq with particular emphasis on integrated development environments, code analysis tools and machine learning.

libcoq-coquelicot

Coq library for real analysis

This package provides a formalization of real analysis compatible with the Coq standard library.