Semantica (2007/2008)

Corso a esaurimento

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

Orario lezioni

3° Q
Giorno Ora Tipo Luogo Note
mercoledì 8.30 - 11.30 lezione Aula E  
venerdì 11.30 - 13.30 lezione Aula B  

Obiettivi formativi

Scopo del corso è quello di introdurre le principali tecniche matematiche usate nello studio dei linguaggi di programmazione:

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

Il corso si rivolge a studenti con uno spiccato interesse per l'informatica teorica.

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 principi di induzione
2.1 induzione matematica, strutturale e ben fondata
2.2 induzione sulle derivazioni
2.3 definizioni per induzione
3 definizioni induttive
3.1 regole e induzione
3.2 regole di prova per la semantica operazionale
3.3 operatori e punti fissi
4 semantica denotazionale linguaggi imperativi
4.1 semantica denotazionale
4.2 confronto con la semantica operazionale
4.3 ordini parziali completi (cpo)
4.4 teorema del punto fisso
5 introduzione alla teoria dei domini
5.1 costruzione di cpo
5.2 un metalinguaggio per la teoria dei domini
6 linguaggi tipati
6.1 tipi
6.2 un linguaggio call-by-value: semantica operazionale e denotazionale
6.3 un linguaggio call-by-name: semantica operazionale e denotazionale
6.4 confronto delle semantiche operazionali e denotazionali

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
G. Winskel The formal Semantics of Programming Languages MIT Press 1993

Modalità d'esame

L'esame consiste in una prova scritta