ITA | ENG
B012511 - TEORIA DEI LINGUAGGI DI PROGRAMMAZIONE
Principali informazioni
Contenuto del corso
Libri di testo consigliati
Obiettivi Formativi
Prerequisiti
Metodi Didattici
Modalità di verifica apprendimento
Programma del corso
Anno Accademico 2013-14
Coorte 2013 - Laurea Magistrale in INFORMATICA
Anno di corso
Primo Anno - Secondo Semestre
Dipartimento di Afferenza
Matematica e Informatica "Ulisse Dini"
Tipo insegnamento
Attività formativa monodisciplinare
Settore Scientifico disciplinare
INF/01 - INFORMATICA
Crediti Formativi
6
Ore Didattica
48
Periodo didattico
03/03/2014 ⇒ 13/06/2014
Frequenza Obbligatoria
No
Tipo Valutazione
Voto Finale
Contenuto del corso
mostra
Programma del corso
mostra
Docenza
Contenuto del corso
Il corso presenta i concetti e le tecniche fondamentali in un approccio fondazionale ai linguaggi di programmazione. Il filo centrale consiste nel vedere sia un singolo programma che un linguaggio completo come un oggetto matematico, sul quale si possono asserire e provare precise proprietà. Argomenti centrali sono: tecniche di semantica operazionale per la definizione formale dei linguaggi, sistemi di tipo e proprietà di correttezza, polimorfismo e sottotipo, fondamenti dei linguaggi orientati
Libri di testo consigliati (Cerca nel catalogo della biblioteca)
Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.
Obiettivi Formativi
Alla fine del corso, gli studenti dovranno aver acquisito le seguenti competenze:
1) Un approccio rigoroso, basato sulla teoria dei tipi, allo studio di problemi connessi al design di linguaggi, alle loro estensioni e implementazioni.
2) Capacità di usare tecniche formali di prova per studiare le proprietà dei programmi.
3) Una preparazione sufficientemente profonda (su semantica e tipi) da consentire l'approfondimento di pubblicazioni di ricerca sui temi trattati.
1) Un approccio rigoroso, basato sulla teoria dei tipi, allo studio di problemi connessi al design di linguaggi, alle loro estensioni e implementazioni.
2) Capacità di usare tecniche formali di prova per studiare le proprietà dei programmi.
3) Una preparazione sufficientemente profonda (su semantica e tipi) da consentire l'approfondimento di pubblicazioni di ricerca sui temi trattati.
Prerequisiti
Prerequisiti raccomandati: Metodi Formali. Corsi avanzati di programmazione. Logica matematica.
Metodi Didattici
Numero di ore per studio personale e altre attività formative di tipo individuale: 90
Numero di ore relative alle attività in aula: 48
Numero di ore relative ad attività seminariali: 12
Numero di ore relative alle attività in aula: 48
Numero di ore relative ad attività seminariali: 12
Modalità di verifica apprendimento
Attività di seminari da parte degli studenti. Esame orale finale.
Programma del corso
Il corso presenta i concetti e le tecniche centrali in uno studio fondazionale dei linguaggi di programmazione, insieme con le loro basi logichee formali. Il filo centrale consiste nel vedere sia un singolo programma che un linguaggio completo come un oggetto matematico, sul quale si possono asserire e provare precise proprietà con tecniche rigorose.
Il programma del corso si articola nei seguenti punti:
1) Fondamenti- Programmazione funzionale, definizioni induttive e metodi formali di prova. Semantica operazionale.
2) Sistemi di tipo- Il lambda-calcolo tipato semplice, le referenze imperative e la type-safety. La metateoria della definizione disottotipo.Algoritmidi type-checking. Polimorfismo e inferenza di tipo.
3) Caso di studio: Featherweight Java (un modello del cuore di java). I tipi generici. La prova di Safety. Tipi intersezione e wildcard.
4) Argomenti avanzati, come i tipi esistenziali e/o il polimorfismo di ordine superiore.
Il programma del corso si articola nei seguenti punti:
1) Fondamenti- Programmazione funzionale, definizioni induttive e metodi formali di prova. Semantica operazionale.
2) Sistemi di tipo- Il lambda-calcolo tipato semplice, le referenze imperative e la type-safety. La metateoria della definizione disottotipo.Algoritmidi type-checking. Polimorfismo e inferenza di tipo.
3) Caso di studio: Featherweight Java (un modello del cuore di java). I tipi generici. La prova di Safety. Tipi intersezione e wildcard.
4) Argomenti avanzati, come i tipi esistenziali e/o il polimorfismo di ordine superiore.