Programmazione funzionale verificata in Agda

Recensioni dei lettori

Il libro è apprezzato come un'introduzione accessibile ai tipi dipendenti utilizzando Agda, in particolare per la dimostrazione pratica dei teoremi. Tuttavia, presenta notevoli carenze in termini di chiarezza, organizzazione e presentazione, che ne compromettono l'efficacia complessiva.

L'introduzione più accessibile ai tipi dipendenti nella pratica, specialmente per Agda.

Prepara i lettori a libri più avanzati sull'argomento.

(basato su 4 recensioni dei lettori)

Titolo originale:

Verified Functional Programming in Agda

Contenuto del libro:

Agda è un linguaggio di programmazione avanzato basato sulla teoria dei tipi. Il sistema di tipi di Agda è abbastanza espressivo da supportare la verifica funzionale completa dei programmi, in due stili.

Nella verifica esterna, scriviamo programmi funzionali puri e poi scriviamo prove di proprietà su di essi. Le prove sono artefatti esterni separati, che in genere utilizzano l'induzione strutturale. Nella verifica interna, specifichiamo le proprietà dei programmi attraverso tipi ricchi per i programmi stessi.

Questo spesso richiede l'inclusione di prove all'interno del codice, per dimostrare al verificatore di tipo che le proprietà specificate sono valide. La possibilità di dimostrare le proprietà dei programmi in questi due stili rappresenta una profonda aggiunta alla pratica della programmazione, in quanto dà ai programmatori la possibilità di garantire l'assenza di bug e quindi di migliorare la qualità del software più di quanto fosse possibile in precedenza. Verified Functional Programming in Agda è il primo libro a fornire un'esposizione sistematica della verifica esterna e interna in Agda, adatta agli studenti universitari di Informatica.

Non si presuppone alcuna familiarità con la programmazione funzionale o con le prove verificate al computer. Il libro inizia con un'introduzione alla programmazione funzionale attraverso esempi familiari come booleani, numeri naturali e liste, e alle tecniche di verifica esterna. La verifica interna viene considerata attraverso gli esempi di vettori, alberi di ricerca binari e alberi di Braun.

Sono inclusi anche materiali più avanzati sul calcolo a livello di tipo, sul ragionamento esplicito sulla terminazione e sulla normalizzazione per valutazione. Il libro include anche un caso di studio di medie dimensioni sulla codifica e decodifica di Huffman.