The version 8.12 has been released (the latest available minor version as of this announcement is 8.12.1) of the interactive theorem proving tool Coq (Rooster).
Coq includes a programming language with dependent types Gallina (Hen), which is based on the theory of calculi of constructions.
The Coq system allows the development of both computer-verifiable proofs of theorems and programs along with their conformance proofs to specifications.
In the new version, the standard library and documentation have been significantly improved, and several bugs have been fixed.
Source: linux.org.ru
