Programy i języki programowania (funkcyjne) będą rozpatrywane jako obiekty matematyczne. Nacisk będzie położony na związki programowania z logiką i dowodami formalnymi (izomorfizm Curry'ego-Howarda). Będą omawiane systemy typów, polimorfizm, podtypowanie, teoretyczne podstawy języków obiektowych.
Jako "język programowania" będzie wykorzystywany przede wszystkim rachunek lambda, ale będą też przykłady w językach Haskell, OCaml, Idris, ...
Wcześniejsza znajomość rachunku lambda ani izomorfizmu Curry'ego-Howarda nie jest wymagana.
Nauczanie zdalne
W razie konieczności możliwe jest przejście na tryb zdalny. Materiały do wykładów będą umieszczane na SKOSie (jak zawsze), a wykład będzie prowadzony on-line z wykorzystaniem wybranej platformy. Zadania na ćwiczenia też będą umieszczane na SKOSie (jak zwykle), rozwiązania studentów będą dostarczane za pośrednictwem SKOSa, a prowadzący zapewni informację zwrotną. Ćwiczenia też będą prowadzone on-line. Wskazani studenci będą prezentowali swoje rozwiązania na forum grupy z możliwością dyskusji.
