Prowadzony w
cyklach:
2024L, 2026Z
Punkty ECTS:
4
Język:
polski
Organizowany przez:
Wydział Matematyki, Informatyki i Mechaniki
Funkcyjne programowanie sieciowe 1000-2M24FPS
1. Podstawy programowania w OCaml-u i Coq-u
2. Typy algebraiczne i zależne
3. Podstawy dowodzenia własności wynikających z typów zależnych
4. Ekstrakcja kodu z efektywnymi typami
5. Pętla komunikacji sieciowej w programach funkcyjnych
6. Parsowanie pakietów binarnych w językach funkcyjnych
7. Logika implementacji protokołu
8. Dowodzenie własności implementacji
Kierunek podstawowy MISMaP
informatyka
Koordynatorzy przedmiotu
Założenia (lista przedmiotów)
Kryteria oceniania
Na podstawie projektu polegającego na implementacji małego protokołu sieciowego w języku funkcyjnym z elementami weryfikacji poprawności pisanego kodu. 100%
Literatura
* Dokumentacja języka programowania Ocaml, https://ocaml.org/docs
* Dokumentacja systemu dowodzenia twierdzeń Coq, https://coq.inria.fr/
* Adam Chlipala, Certified Programming with Dependent Types, http://adam.chlipala.net/cpdt/