Matija Pretnar: λ-račun s tipi

Povzetek. λ-račun, ki smo ga spoznali zadnjič, bomo opremili s tipi in s tem dobili veliko bolj pohleven jezik. To bomo podkrepili tudi z dokazom, da iz vsakega programa, ki ima tip, lahko izračunamo vrednost. Taki programi torej ne morejo divergirati ali povzročiti napak pri izvajanju.