Coq 8.12

Излезе версия 8.12 (последната налична минорна версия към момента на публикуване на новината – 8.12.1) на инструмента за интерактивно доказване на теореми Coq (петел).

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

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

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

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