A01 Wprowadzenie do formalnych dowodów na komputerze

Najprostszym materiałem wprowadzającym do języka Coq, w którym pisane są sformalizowane dowody na tej stronie, są kilkunastominutowe filmiki nagrane przez A. Bauera i dostępne na youtubie.


Innym dość prostym źródłem jest kurs autorstwa Thorstena Altenkircha z University of Nottingham.


Ciekawą, prosto napisaną książką na temat podstaw programowania i podstaw logiki, napisaną w Coq-u (cała książka to komentarze i kod źródłowy) jest Software Foundations. W książce jest zaimplementowane szereg klasycznych konstrukcji matematycznych.


Dokumentacja Coq- jest tam podręcznik użytkownika oraz szereg odnośników rozszerzających powyższą listę, która jest zredagowana z intencją, żeby zaprezentować źródła od najprostszych do najbardziej wyszukanych.

Created with Madoko.net.