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
Prerequisites
Course coordinators
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/
Additional information
Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:
- Bachelor's degree, first cycle programme, Computer Science
- Master's degree, second cycle programme, Computer Science
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: