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

ćwiczenia5        
 

6. Więcej typów zależnych

ćwiczenia6        
 

7. Indeksowane struktury danych

ćwiczenia7        
 

8. Zadanie zaliczeniowe 2

zadanie zaliczeniowe 2        

Termin wykonania: 26 maja (2 tygodnie)  

9. Rekurencja

ćwiczenia9        
 

10. Type classes i uogólnione przepisywanie

ćwiczenia10        
 

11. Zadanie zaliczeniowe 3

zadanie zaliczeniowe 3        

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