Calcolo lambda e modelli formali della computazione

Modulo 1: La Computazione Formale Storia della teoria della computazione Modelli di computazione: macchina di Turing, calcolo lambda, automi Modulo 2: Nozioni di Base del Calcolo Lambda Definizione di calcolo lambda Espressioni lambda e sintassi Tipologie di variabili e funzioni anonime Modulo 3: Riduzione e Strategie di Valutazione Beta-riduzione e alpha-conversione Strategie di valutazione: normale, applicativa, call-by-name, call-by-value Modulo 4: Calcolo Lambda Tipato Tipi semplici nel calcolo lambda Sistema di tipi e inferenza di tipo Relazione con i linguaggi di programmazione Modulo 5: Lambda Calculus e Funzioni Ricorsive Definizione di funzioni ricorsive Operatore Y per la ricorsione Modulo 6: Relazione tra Lambda Calculus e Macchine di Turing Equivalenza tra calcolo lambda e macchine di Turing Concetto di Turing-completezza Relazione con la teoria della computabilità Modulo 7: Modelli Formali della Computazione Macchine di Turing: definizione e varianti Automi finiti e macchine a stati Calcolo combinatorio Modulo 8: Logica e Lambda Calculus Relazione tra logica e calcolo lambda Interpretazione di logica proposizionale e predicativa Isomorfismo di Curry-Howard Modulo 9: Lambda Calculus e Linguaggi di Programmazione Programmazione funzionale Linguaggi basati su calcolo lambda: Haskell, Lisp, ML Ottimizzazione e compilazione Modulo 10: Lambda Calculus e Teoria delle Categorie Categorie e funtori Monadi e loro applicazioni nel calcolo lambda Concetto di morfismi computazionali Modulo 11: Estensioni del Calcolo Lambda Lambda-calcolo tipato con polimorfismo Lambda-calcolo con effetti laterali Lambda-calcolo con tipi dipendenti Modulo 12: Teoria della Complessità e Computabilità Problemi decidibili e indecidibili Complessità computazionale e classi di complessità Relazione tra complessità e modelli formali Modulo 13: Lambda Calculus nella Verifica Formale Uso del calcolo lambda nella verifica di programmi Metodi formali e proof assistants (Coq, Agda) Modulo 14: Applicazioni del Calcolo Lambda Analisi statica e ottimizzazione del codice Uso nei compilatori e interpreti Blockchain e smart contracts basati su lambda calculus Modulo 15: Progetti e Approfondimenti Implementazione di un piccolo interprete lambda Prospettive future del calcolo lambda nella computazione.