Programowanie z typami zależnymi i dowodzenie twierdzeń - laboratorium

System Coq wraz z dokumentacją dostępny jest pod adresem http://coq.inria.fr

1. Zapoznanie sie z systemem, podstawowe komendy, taktyki...

wręczałt ćwiczenia1 przykładowe rozwiązania

2. Definicje indukcyjne

ćwiczenia2 przykładowe rozwiazania

3. Dowody różne

ćwiczenia3 przykładowe rozwiązania

4. Zadanie zaliczeniowe 1

zadanie zaliczeniowe 1 przykładowe rozwiazanie

5. Inwersja, typy zależne

6. Więcej typów zależnych

7. Indeksowane struktury danych

8. Zadanie zaliczeniowe 2

zadanie zaliczeniowe 2

Termin wykonania: 26 maja (2 tygodnie)

9. Rekurencja

10. Type classes i uogólnione przepisywanie

11. Zadanie zaliczeniowe 3

zadanie zaliczeniowe 3

Termin wykonania: 30 czerwca (do końca sesji)