Calculul Lambda cu tipuri

Recenzii ale cititorilor

În prezent, nu există recenzii ale cititorilor. Evaluarea se bazează pe 3 voturi.

Titlul original:

Lambda Calculus with Types

Conținutul cărții:

Acest manual cu exerciții dezvăluie în formalisme, folosite până acum mai ales pentru proiectarea și verificarea hardware și software, o frumusețe matematică neașteptată. Calculul lambda formează un prototip de limbaj de programare universal, care în versiunea sa netipată este înrudit cu Lisp și a fost tratat în clasicul The Lambda Calculus (1984) al primului autor.

De atunci, formalismul a fost extins cu tipuri și utilizat în programarea funcțională (Haskell, Clean) și în asistenții de demonstrație (Coq, Isabelle, HOL), folosiți în proiectarea și verificarea produselor IT și a demonstrațiilor matematice. În această carte, autorii se concentrează asupra a trei clase de tipărire pentru termenii lambda: tipuri simple, tipuri recursive și tipuri de intersecție.

În aceste trei formalisme de termeni și tipuri se dezvăluie frumusețea matematică neașteptată. Tratarea este autoritară și cuprinzătoare, completată de o bibliografie exhaustivă, iar numeroase exerciții sunt oferite pentru a aprofunda înțelegerea cititorilor și pentru a le spori încrederea în utilizarea tipurilor.