CoqIDE Proof Assistant
proof assistant for higher-order logic (gtk interface)
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.
This package provides CoqIde, a graphical user interface for
developing proofs.
- Homepage
- http://coq.inria.fr/
- Package
- coqide | source