Celem przedmiotu jest zaprezentowanie podstaw rachunku lambda, formalizmu stanowiącego jeden z najważniejszych modeli obliczeń, który dodatkowo leży u podstaw większości dobrze zaprojektowanych języków programowania. Skupimy się na formalnym i możliwie dogłębnym omówieniu kilku fundamentalnych zagadnień, takich jak:
* lambda-teorie i ich własności
* twierdzenie Churcha-Rossera
* standardyzacja redukcji
* postaci czołowo-normalne i drzewa Böhma
* logika kombinatorów (opcjonalnie)
* lambda-wyrażalność i obliczalność
* modele rachunku lambda
* typy i silna normalizacja
* implementacje rachunku lambda
