## 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.