CoQ 8.12

Версия 8.12 (най-новата налична второстепенна версия към момента на писане е 8.12.1) на интерактивната програма за доказване на теорема Coq (петел) беше пусната.

Coq включва език за програмиране със зависими типове Gallina (пиле), базиран на теорията на строителното смятане.

Системата Coq ви позволява да разработите както компютърно проверими доказателства за теореми, така и програми, заедно с доказателство за съответствие със спецификацията.

Новата версия значително подобри стандартната библиотека и документация и поправи редица грешки.

Източник: linux.org.ru