Tipuri de rafinare: Un tutorial

Titlul original:

Refinement Types: A Tutorial

Conținutul cărții:

Tipurile de rafinare pot fi vectorul care aduce verificarea formală în dezvoltarea de software de masă. Acest rezultat fericit depinde de proiectarea și punerea în aplicare a sistemelor de tipuri de rafinament care pot fi adaptate la limbajele existente sau coproiectate cu unele noi.

În această carte, autorii catalizează dezvoltarea unor astfel de sisteme prin distilarea ideilor dezvoltate în literatura vastă pe această temă într-un tutorial coerent și unificat care explică ingredientele cheie ale sistemelor moderne de tip refinament, arătând cum se implementează un verificator de tip refinament.

Inspirați de cadrul nanopass pentru predarea compilației, autorii arată cum se implementează tipurile de rafinament prin intermediul unei progresii de limbaje care adaugă treptat caracteristici limbajului sau sistemului de tipuri.

Cartea ușor accesibilă oferă cititorului o introducere pătrunzătoare în tipurile de rafinare folosind un stil tutorial inovator care permite învățarea rapidă. În plus, implementarea software însoțitoare permite cititorilor să lucreze pe exemple practice din lumea reală.