Wykład z Coqa

Strona laboratorium

Wykład 1: Dowodzenie w Coqu - wstęp i przykłady
Wyklad 2: Rachunek Konstrukcji - termy, typy, polimorfizm, zależności...
Wykład 3: Definicje indukcyjne w Coqu
Wykład 4: Definicje indukcyjne w Coqu (bliżej praktyki)
Wykład 5: W przód i w tył (czyli taktyki)
Wyklad 6: Poza Rachunek Konstrukcji: PTS, ECC, uniwersa w Coqu
Wykład 7: Uniwersa i typy indukcyjne
Wykład 8: Środowisko, sekcje, moduły
Wykład 9: Interpretacje symboli, język taktyk
Wykład 10: Refleksja, specyfikacje funkcji
Wykład 11: Ekstrakcja, rekursja ogólna
Wykład 12: Jeszcze o rekursji i indukcji
Wykład 13: O obiektach nieskończonych: typy koindukcyjne
Wykład 14: Dowodzenie własności programów imperatywnych

Inne materiały na temat Coqa

"Obliczenia i wnioskowanie w systemie Coq" -- materiały do wykładu na Uniwersytecie Wrocławskim