Advanced functional programming 1000-2M11ZPF
1. Types and type classes (ca 3 weeks)
• Algebraic data types and type classes
• Constructor classes
• Multi-parameter classes, functional dependencies
• Type families. Associated types, generalised algebraic datatypes (GADT)
2. Specifying and testing Haskell programs
Parallel programming in Haskell
• Multi-core and multi-processor programming (SMP)
• Data parallelism (Data Parallel Haskell)
3. Programming with dependent types in Idris
4. Programming with dependent types in Coq
5. Program verification and theorem proving in Coq
6. Parallel programming in Haskell
Main fields of studies for MISMaP
Type of course
Requirements
Course coordinators
Learning outcomes
Knowledge
1. has profound knowledge of functional programming
2. knows methods of functional language specification
3. knows methods of parallel programm in a functional language
Abilities
1. is able to design a middle-size functional program
2. is able to use types to specify and verify programs
3. is able to apply functional program parallalisation techniques
Social competences
1. knows limits of own knowledge and understand the need of further education
2. is able to precisely formulate questions, destined to improve understanding of the subject
3. understands the need of systematic work on all long-term projects
Assessment criteria
Final grade based on lab assignments and their presentation.
Bibliography
1. B. O'Sullivan, J. Goerzen, D. Stewart Real World Haskell O'Reilly Media 2008, http://book.realworldhaskell.org/
2. Adam Chlipala, Certified Programming with Dependent Types, A
Pragmatic Introduction to the Coq Proof Assistant, MIT Press 2013,
http://adam.chlipala.net/cpdt/
3. Yves Bertot, Pierre Castéran, Interactive Theorem Proving and
Program Development Coq'Art: The Calculus of Inductive Constructions,
Springer 2004, https://www.labri.fr/perso/casteran/CoqArt/
4. Simon Marlow, Parallel and Concurrent Programming in Haskell, O'Reilly Media 2013,
http://chimera.labs.oreilly.com/books/1230000000929/
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: