Conducted in
terms:
2024L, 2026Z
ECTS credits:
4
Language:
Polish
Organized by:
Faculty of Mathematics, Informatics, and Mechanics
Network programming in functional languages 1000-2M24FPS
1. Basics of programming in OCaml and Coq
2. Algebraic and dependent types
3. Basics of proving of properties resulting from dependent types
4. Code extraction with effective types
5. Communication loop in functional languages
6. Binary packet parsing in functional languages
7. Logic of program implementation
8. Proving of program properties
Main fields of studies for MISMaP
computer science
Course coordinators
Prerequisites
Assessment criteria
Based upon a project that consists in implementation of a small netwok protocol in functional language with elements of program verification - 100%
Bibliography
* Documentation of OCaml, https://ocaml.org/docs
* Documentation of Coq, https://coq.inria.fr/
* Adam Chlipala, Certified Programming with Dependent Types, http://adam.chlipala.net/cpdt/