Podstawy języków programowania w systemie Coq
| Semestr zimowy 2014/15 |
| Dariusz Biernacki |
| Środa 10:15-14:00 |
| Sala 140 (wykład), 137 (pracownia) |
| 6 ECTS |
Przedmiot stanowi wprowadzenie do matematycznych podstaw
niezawodnego oprogramowania. Poruszana tematyka dotyczy
wybranych elementów teorii języków programowania, a całość
przedmiotu realizowana jest w oparciu o podręcznik
Software
Foundations, przy czym wszystkie zagadnienia omawiane
są w formalizmie systemu Coq.
|
Co nowego?
|
Materiały do wykładu
|
Terminarz
|
Terminy i tematy wykładów, odsyłacze
do literatury, listy zadań, etc. |
|
Literatura
|
Podręczniki oraz literatura uzupełniająca |
|
Dodatkowe zasoby
|
Implementacje i oprogramowanie wspomagające wykład |
|
Regulamin
|
Regulamin przedmiotu |
|
Informacje o wykładzie
| Wykład |
Środa 10:15-12:00, s. 140 |
| Konsultacje |
Wtorek 14:15-16:00 |
| Pracownia |
Środa 12:15-14:00, s. 137 |
| Podręcznik |
Software
Foundations
|
| ECTS |
6 |
| Liczba godzin |
30h wykładu + 30h pracowni |
| Ocena z przedmiotu |
3 prace domowe (pierwsza -- 20%, pozostałe -- po 40%) |
| Prace domowe |
Listy zadań do zrealizowania w systemie Coq
|
| Tematy |
podstawy logiki
komputerowo wspomagane dowodzenie twierdzeń (system Coq)
programowanie funkcyjne
semantyka operacyjna
logika Hoare'a
statyczne systemy typów
|
| Strona domowa |
http://www.ii.uni.wroc.pl/~dabi/courses/PJP14
|
|