Die Version 8.12 (die zuletzt verfügbare Minor-Version zum Zeitpunkt der Veröffentlichung dieser Nachricht ist 8.12.1) des interaktiven Theorembeweisers Coq (Hahn) wurde veröffentlicht.
Coq beinhaltet die Programmiersprache mit abhängigen Typen Gallina (Huhn), die auf der Theorie der Typkalküle basiert.
Das Coq-System ermöglicht die Entwicklung sowohl computergestützter, überprüfbarer Theoremdemonstrationen als auch Programme zusammen mit dem Nachweis der Einhaltung von Spezifikationen.
In der neuen Version wurde die Standardbibliothek und die Dokumentation erheblich überarbeitet, und es wurden mehrere Fehler behoben.
Quelle: linux.org.ru
