Semantica (2008/2009)

Corso a esaurimento

Codice insegnamento
4S00065
Docente
Andrea Masini
crediti
5
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Periodo
3° Q dal 20-apr-2009 al 19-giu-2009.

Orario lezioni

3° Q
Giorno Ora Tipo Luogo Note
giovedì 15.30 - 17.30 lezione Aula F  
venerdì 10.30 - 13.30 lezione Aula F  

Obiettivi formativi

Il corso introduce le principali tecniche sviluppate nell'area della "semantica formale dei linguaggi di programmazione":

* sistemi di tipi
* semantica operazionale
* domini
* semantica denotazionale


Il corso presuppone le competenze acquisite nei corsi di "Programmazione", "Logica", "Algebra", "Linguaggi di Programmazione" e "Fondamenti dell'informatica" della laurea triennale in informatica.

Programma

1 semantica operazionale
1.1 definizione di un semplice linguaggio imperativo
1.2 regole di valutazione

2 induzione
2.1 induzione matematica
2.2 induzione strutturale
2.3 induzione ben fondata

3 semantica denotazionale dei linguaggi imperativi
3.1 composizionalita'
3.2 il caso dei programmi senza while
3.3 il trattamento del while

4 introduzione alla teoria dei domini
4.1 ordini parziali completi
4.2 continuita'
4.3 il teorema di Knaster-Tarski
4.4 costruzione di domini:
domini prodotto; domini di funzioni; domini piatti
5 PCF
5.1 termini e tipi
5.2 variabbili liberee legate; sostituzione
5.3 tipaggio
5.4 valutazione (semantica operazionale)

6 semantica denotazionale di PCF
6.1 denotazione dei termini
6.2 denotazione dei termini
6.3 composizionalita'
6.4 correttezza

Modalità d'esame

L'esame consiste in una prova scritta

Materiale didattico

Documenti