Introduzione ai tipi dipendenti con Idris: codificare le prove dei programmi nei tipi

Recensioni dei lettori

Attualmente non ci sono recensioni dei lettori. La valutazione si basa su 2 voti.

Titolo originale:

Introduction to Dependent Types with Idris: Encoding Program Proofs in Types

Contenuto del libro:

I tipi dipendenti sono un concetto che consente agli sviluppatori di scrivere codice che porta con sé delle prove. Idris è un linguaggio di programmazione che supporta i tipi dipendenti. Questo libro vi insegnerà le basi matematiche di Idris e come usarlo per scrivere software e dimostrare matematicamente le proprietà.

La prima parte del libro funge da introduzione alle teorie di base del linguaggio. Inizia con una rassegna dei sistemi formali e dei sistemi logici matematici come elementi fondamentali, per poi arrivare gradualmente ai tipi dipendenti. Successivamente, si apprende la teoria dei tipi per i tipi dipendenti. In seguito, si esplorerà il linguaggio di programmazione Idris e si concluderà esplorando le profondità dei sistemi formali e dei type checker implementandoli.

Introduzione ai tipi dipendenti con Idris vi guiderà attraverso semplici esempi fino a tecniche più avanzate, aumentando la difficoltà man mano che acquisite conoscenze. Ogni capitolo comprende una serie di esercizi basati su ciò che è stato trattato per consolidare ulteriormente l'apprendimento. Non è prevista alcuna conoscenza specialistica della matematica al di là delle nozioni di base, quindi è perfetto per i principianti.

Che cosa imparerete?

Comprendere il calcolo Lambda e i tipi dipendenti.

⬤ Acquisire una visione della programmazione funzionale.

⬤ Scrivere prove matematiche con Idris.

Per chi è questo libro?

Programmatori, matematici, accademici e chiunque sia interessato a imparare i tipi dipendenti e il calcolo lambda.