Programmazione dichiarativa
A.A. 2023/2024
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 può essere seguito come corso singolo.
Programma e organizzazione didattica
Edizione unica
Responsabile
Periodo
Secondo semestre
Programma
Parte 1: il paradigma funzionale
Linguaggio usato: F#
1.1 Intro
- il paradigma, basi di 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
1.2 Case studies
1.2.1 Type checking and type inference - si parte da soliti type checkers per
espressioni aritmetiche per arrivare a type inference del lambda calcolo
--------------------------------------------
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
Linguaggio usato: F#
1.1 Intro
- il paradigma, basi di 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
1.2 Case studies
1.2.1 Type checking and type inference - si parte da soliti type checkers per
espressioni aritmetiche per arrivare a type inference del lambda calcolo
--------------------------------------------
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://amomiglianopd.ariel.ctu.unimi.it/v5/home/Default.aspx
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/
https://amomiglianopd.ariel.ctu.unimi.it/v5/home/Default.aspx
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
Siti didattici
Docente/i