Funkcyjne programowanie sieciowe
Informacje ogólne
Kod przedmiotu: | 1000-2M24FPS |
Kod Erasmus / ISCED: | (brak danych) / (brak danych) |
Nazwa przedmiotu: | Funkcyjne programowanie sieciowe |
Jednostka: | Wydział Matematyki, Informatyki i Mechaniki |
Grupy: |
Przedmioty obieralne dla informatyki Przedmioty obieralne narzędziowe dla informatyki |
Punkty ECTS i inne: |
4.00
|
Język prowadzenia: | (brak danych) |
Założenia (lista przedmiotów): | Podstawy matematyki 1000-211bPM |
Skrócony opis: |
Przedmiot ma na celu przedstawienie zaawansowanych mechanizmów programowania funkcyjnego z typami zależnymi na przykładzie tworzenia klienta i serwera protokołu sieciowego. Na zajęciach wykorzystywane będzie programowanie funkcyjne w Ocamlu wzbogacone o elementy weryfikacji funkcyjnych własności wykonywane w Coq-u. |
Pełny opis: |
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 |
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/ |
Metody i 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% |
Zajęcia w cyklu "Semestr letni 2024/25" (jeszcze nie rozpoczęty)
Okres: | 2025-02-17 - 2025-06-08 |
Przejdź do planu
PN WT ŚR CZ PT |
Typ zajęć: |
Laboratorium, 30 godzin
|
|
Koordynatorzy: | Aleksy Schubert | |
Prowadzący grup: | Aleksy Schubert | |
Lista studentów: | (nie masz dostępu) | |
Zaliczenie: | Zaliczenie na ocenę |
Właścicielem praw autorskich jest Uniwersytet Warszawski.