Hodnotenie:
Momentálne nie sú žiadne recenzie čitateľov. Hodnotenie je založené na 3 hlasoch.
Lambda Calculus with Types
Táto príručka s cvičeniami odhaľuje vo formalizmoch, ktoré sa doteraz používali najmä na návrh a verifikáciu hardvéru a softvéru, nečakanú matematickú krásu. Lambda kalkul tvorí prototyp univerzálneho programovacieho jazyka, ktorý je vo svojej netypizovanej verzii príbuzný s Lispom a ktorý bol spracovaný v klasickej knihe prvého autora The Lambda Calculus (1984).
Formalizmus bol odvtedy rozšírený o typy a používa sa vo funkcionálnom programovaní (Haskell, Clean) a v asistentoch dôkazov (Coq, Isabelle, HOL), ktoré sa používajú pri návrhu a verifikácii IT produktov a matematických dôkazov. V tejto knihe sa autori zameriavajú na tri triedy typizácie pre lambda výrazy: jednoduché typy, rekurzívne typy a priesečníkové typy.
Práve v týchto troch formalizmoch termov a typov sa odhaľuje nečakaná matematická krása. Spracovanie je autoritatívne a vyčerpávajúce, doplnené vyčerpávajúcou bibliografiou, a na prehĺbenie pochopenia čitateľov a zvýšenie ich istoty pri používaní typov sú k dispozícii početné cvičenia.
