Lambda kalkul s typy

Recenze čtenářů

Aktuálně nejsou k dispozici žádné recenze čtenářů. Hodnocení je založeno na 3 hlasů.

Původní název:

Lambda Calculus with Types

Obsah knihy:

Tato příručka s cvičeními odhaluje ve formalismech, dosud používaných především pro návrh a verifikaci hardwaru a softwaru, nečekanou matematickou krásu. Lambda kalkul tvoří prototyp univerzálního programovacího jazyka, který je ve své netypizované verzi příbuzný s Lispem a byl zpracován v autorově klasické knize The Lambda Calculus (1984).

Od té doby byl formalismus rozšířen o typy a použit ve funkcionálním programování (Haskell, Clean) a v důkazových asistentech (Coq, Isabelle, HOL), používaných při návrhu a ověřování IT produktů a matematických důkazů. V této knize se autoři zaměřují na tři třídy typování lambda výrazů: jednoduché typy, rekurzivní typy a typy průniků.

Právě v těchto třech formalismech termínů a typů se odhaluje nečekaná matematická krása. Pojednání je autoritativní a vyčerpávající, doplněné vyčerpávající bibliografií, a k prohloubení porozumění čtenářů a zvýšení jejich jistoty při používání typů jsou uvedena četná cvičení.