Programmazione dichiarativa
A.A. 2025/2026
Obiettivi formativi
Lo scopo dell'insegnamento è fornire agli studenti una solida conoscenza della programmazione dichiarativa, nella sue declinazioni di programmazione funzionale e programmazione logica. L'insegnamento è organizzato intorno all'idea della programmazione relazionale come una estensione del paradigma funzionale. Le applicazioni che studieremo sono legate alla dimostrazione automatica e la semantica dei linguaggi di programmazione.
Risultati apprendimento attesi
Lo studente sarà in grado di scrivere programmi di media complessità in ambo i paradigmi e di apprezzarne la complementarietà.
Periodo: Secondo semestre
Modalità di valutazione: Esame
Giudizio di valutazione: voto verbalizzato in trentesimi
Corso singolo
Questo insegnamento non può essere seguito come corso singolo. Puoi trovare gli insegnamenti disponibili consultando il catalogo corsi singoli.
Programma e organizzazione didattica
Edizione unica
Responsabile
Periodo
Secondo semestre
Programma
Esploreremo il paradigma della programmazione funzionale e della sua verifica e convalida
Prima parte: Linguaggio usato: F#
- ricorsione e iterazione
- tipi e poliformisfmo
- tipi di dati algebrici
- property based testing
- funzioni higher horder
- lazy evaluation e tail recursion
- monadi e continuazioni
Seconda parte: programmazione "correct-by-construction" usando F*
- Contratti & refinement types (RT)
- RT per la parzialità
- dimostrare programmi terminanti
- model based reasoning
- cenni sulla logica degli SMT
- polimorfismo, equality types, definitional equality
- tipi di dati astratti e ragionamento equazionale
Prima parte: Linguaggio usato: F#
- ricorsione e iterazione
- tipi e poliformisfmo
- tipi di dati algebrici
- property based testing
- funzioni higher horder
- lazy evaluation e tail recursion
- monadi e continuazioni
Seconda parte: programmazione "correct-by-construction" usando F*
- Contratti & refinement types (RT)
- RT per la parzialità
- dimostrare programmi terminanti
- model based reasoning
- cenni sulla logica degli SMT
- polimorfismo, equality types, definitional equality
- tipi di dati astratti e ragionamento equazionale
Prerequisiti
Nessuno. E' consigliato il superamento degli esami di Logica, Programmazione 1 e 2 e Algoritmi.
Metodi didattici
Lezioni in presenza frontali e laboratorio
Materiale di riferimento
Pagina web
https://myariel.unimi.it/mod/folder/view.php?id=38751
Bibliografia:
Parte 1: Functional Programming using F# , Michael R. Hansen and Hans Rischel.
Parte 2: online book Proof-oriented Programming In F*
https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf
https://myariel.unimi.it/mod/folder/view.php?id=38751
Bibliografia:
Parte 1: Functional Programming using F# , Michael R. Hansen and Hans Rischel.
Parte 2: online book Proof-oriented Programming In F*
https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf
Modalità di verifica dell’apprendimento e criteri di valutazione
L'esame consiste di una prova in laboratorio su PC di durata di circa 3 ore (tre), e richiede la scrittura di programmi relativi agli argomenti trattati nell'insegnamento. La valutazione, che verrà comunicata anonimizzata sul ariel, è espressa in trentesimi e dipende dalla correttezza ed eleganza delle soluzioni offerte.
INF/01 - INFORMATICA - CFU: 6
Lezioni: 48 ore
Docente/i