The Coq Proof Assistant
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.
Coq Integrated Development Environment
The Coq Integrated Development Environment (coqide) is a graphical development environment for Coq. It allows the user to navigate within a Coq vernacular file, executing corresponding commands or undoing them respectively.
Proof General
An Emacs-based generic front-end for proof assistants.
Coq Survival Kit (Pichardie and Blazy)
Some nice slides showing what the most useful Coq tactics do.
Software Foundations (Pierce et al.)
Topics include basic concepts of logic, computer-assisted theorem proving, the Coq proof assistant, functional programming, operational semantics, Hoare logic, and static type systems. The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity will be helpful.