Programmazione dichiarativa

A.A. 2024/2025
6
Crediti massimi
48
Ore totali
SSD
INF/01
Lingua
Italiano
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à.
Corso singolo

Questo insegnamento può essere seguito come corso singolo.

Programma e organizzazione didattica

Edizione unica

Periodo
Secondo semestre

Programma
Parte 1: il paradigma funzionale
Linguaggio usato: F#
- ricorsione e iterazione
- tipi e poliformisfmo
- tipi di dati algebrici
- property based testing
- funzioni higher horder
- lazy evaluation
- tipi di dati astratti
- monadi e continuazioni

--------------------------------------------
Parte 2: il paradigma relazionale:

Linguaggio usato: Twelf

- fatti, regole e queries
- unificazione e proof search
- esempi:
+ rappresentazione conoscenza ...
+ esempi combinatoriali come 8 regine
+ automi non deterministici
- analisi statica di programmi logici: mode, coverage e termination checking
- esempi legati alla teoria dei linguaggi di programmazione:

+ interpreti e type checkers da lambda calcolo base
fino a un modello di MiniML
+ uso di tipi dipendenti per scrivere interpreti e macchine astratte
type preserving
Prerequisiti
Nessuno. E' fortemente consigliato il superamento degli esami di Logica, Programmazione 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

Bibiografia:
Parte 1: Functional Programming using F# , Michael R. Hansen and Hans Rischel.

Parte 2: Dispense di Fiorentini e slides
Riferimenti addizionali: Frank Pfenning:
Logic programming https://www.cs.cmu.edu/~fp/courses/lp/
Computation and Deduction https://www.cs.cmu.edu/~fp/courses/comp-ded/
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
Ricevimento:
Su appuntamento
vedi https://fiorentini.di.unimi.it/
Ricevimento:
su appuntamento
4009, Celoria 18