Refinement Types: A Tutorial
A finomítási típusok lehetnek az a vektor, amely a formális verifikációt a szoftverfejlesztés főáramába emeli. Ez a szerencsés kimenetel a meglévő nyelvekbe utólagosan beépíthető vagy új nyelvekkel együtt tervezhető finomítási típusrendszerek tervezésén és megvalósításán múlik.
Ebben a könyvben a szerzők katalizálják az ilyen rendszerek fejlesztését azáltal, hogy a témával kapcsolatos burjánzó szakirodalomban kidolgozott ötleteket egy koherens és egységes útmutatóba foglalják, amely a modern finomítási típusrendszerek legfontosabb összetevőit magyarázza el, bemutatva, hogyan kell egy finomítási típusellenőrzőt megvalósítani.
A fordítás tanítására szolgáló nanopass keretrendszer által inspirálva a szerzők bemutatják, hogyan lehet finomító típusokat implementálni a nyelvek progresszióján keresztül, amelyek fokozatosan adnak hozzá funkciókat a nyelvhez vagy a típusrendszerhez.
A könnyen hozzáférhető könyv a gyors tanulást lehetővé tevő, innovatív oktatói stílus segítségével nyújt az olvasónak éleslátó bevezetést a finomítási típusokba. Továbbá a kísérő szoftveres megvalósítás lehetővé teszi az olvasók számára, hogy gyakorlati, valós példákon dolgozzanak.