Tipi di raffinamento: Un tutorial

Titolo originale:

Refinement Types: A Tutorial

Contenuto del libro:

I tipi di raffinamento possono essere il vettore che porta la verifica formale nello sviluppo del software tradizionale. Questo felice risultato dipende dalla progettazione e dall'implementazione di sistemi di tipi di raffinamento che possono essere adattati ai linguaggi esistenti o co-progettati con quelli nuovi.

In questo libro, gli autori catalizzano lo sviluppo di tali sistemi distillando le idee sviluppate nella vasta letteratura sull'argomento in un tutorial coerente e unificato che spiega gli ingredienti chiave dei moderni sistemi di tipo refinement, mostrando come implementare un verificatore di tipo refinement.

Ispirandosi al framework nanopass per l'insegnamento della compilazione, gli autori mostrano come implementare i tipi di raffinamento attraverso una progressione di linguaggi che aggiungono incrementalmente caratteristiche al linguaggio o al sistema di tipi.

Il libro, facilmente accessibile, fornisce al lettore un'introduzione approfondita ai tipi di raffinamento utilizzando uno stile tutoriale innovativo che consente un rapido apprendimento. Inoltre, l'implementazione del software che lo accompagna permette ai lettori di lavorare su esempi pratici del mondo reale.