Matija Pretnar: Izpeljava tipov

Povzetek. Po tem, ko bomo odpravili stare dolgove (dokaz krepke normalizacije λ-računa s tipi), bomo našteli še nekaj možnih razširitev λ-računa (seznami, lokalno prirejanje, rekurzija, vsote, …), nato pa bomo pokazali, kako izračunamo najbolj splošen tip danega izraza (če ga izraz seveda sploh ima).