Home | Search | Help  
Home Page Università di Genova

Corso di Informatica Teorica, Calcolabilità e Complessità (Mod.2) (Laurea Magistrale LM-18)

Docente: Elena Zucca

Lo scopo del corso è fornire allo studente una conoscenza di base dei fondamenti dei linguaggi di programmazione, in particolare sistemi di tipo, semantica e correttezza.

AulaWeb a.a. 11/12

AulaWeb a.a. 10/11

AulaWeb a.a. 09/10

Modalità d'esame

L'esame consta di una prova scritta e una prova orale. Per sostenere l'orale occorre aver superato lo scritto (almeno 18). Un voto sufficiente allo scritto può essere conservato per i due appelli successivi (non viene conservato in caso di orale fallito).

Le modalità d'esame per il corso disattivato di Informatica Teorica (Laurea Specialistica ad esaurimento) sono le stesse.

Programma

  • Preliminari: sistemi induttivi e definizioni induttive, principio di induzione (generale), casi particolari (induzione aritmetica e induzione aritmetica completa), sistemi induttivi multipli e relativo principio di induzione, definizioni induttive multiple, grammatiche come caso particolare di definizioni induttive. Definizione di un linguaggio come famiglia (algebra) di termini su una segnatura, principio di induzione strutturale. Testi di riferimento: note parte 1.
  • Semantica operazionale: macchine astratte, semantica operazionale small-step di un linguaggio di espressioni booleane e naturali, alberi di prova, prove per induzione sulla definizione della relazione di riduzione, forme normali e termini stuck. Prova di terminazione della relazione di riduzione per il linguaggio delle espressioni. Introduzione al lambda calcolo: lambda calcolo puro, semantica operazione call-by-value, strategie di valutazione alternative. Currying, booleani di Church, numerali di Church. Non terminazione e ricorsione. Testi di riferimento: note parti 2 e 3, per approfondimenti libro Pierce capitoli 3 e 5.
  • Sistemi di tipi: sistema di tipi per il linguaggio di espressioni booleane e naturali, prova dei teoremi di progress e di conservazione dei tipi. Sistema di tipi semplici per il lambda-calcolo, prova dei teoremi di progress e di conservazione dei tipi. Estensioni sintattiche al lambda-calcolo tipato (tipo Unit, sequenza, coppie, let-in, operatore di punto fisso tipato, riferimenti, eccezioni). Testi di riferimento: note parte 4 e 5, per approfondimenti libro Pierce capitoli 8, 9, 11, 13, 14.
  • Featherweight Java: introduzione, esempi, regole di riduzione, cenni al sistema di tipi e alla soundness. Testi di riferimento: note parte 6, per approfondimenti libro Pierce capitolo 19.
  • Semantica denotazionale: principi, semantica denotazionale di un linguaggio imperativo. Testi di riferimento: note parte 7.
  • Asserzioni per linguaggi imperativi, deduzione alla Hoare. Testi di riferimento: note parte 8, per approfondimenti articolo Nielson&Nielson.

Testi di riferimento

Sono disponibili le note delle lezioni, necessarie e sufficienti per la preparazione dell'esame.

La parte su semantica operazionale dei linguaggi, lambda calcolo, sistemi di tipo, Featherweight Java segue sostanzialmente il libro "Types and Programming Languages" di B. Pierce, disponibile in biblioteca. Dal sito del libro è anche possibile scaricare delle implementazioni in OCaml di alcuni calcoli presentati nel corso (espressioni naturali e booleane, lambda calcolo). Se avete voglia e tempo, fare un po' di sperimentazione con queste implementazioni è molto istruttivo.

Per la parte sulle asserzioni alla Hoare potete anche consultare: Axiomatic Program Verification (estratto da "Semantics with Applications - A Formal Introduction", H.R. Nielson e F. Nielson, edizione rivista, 1999; prima edizione del 1992 pubblicata da John Wiley & Sons). Per i curiosi, un po' di materiale su JML (Java Modeling Language), un linguaggio di specifica per Java basato su tecniche alla Hoare: lucidi (un po' vecchi) e home page di JML.

Esempi di esercizi d'esame

Fate riferimento principalmente ai testi d'esame degli anni accademici precedenti che trovate qui. Inoltre:
  • su semantica operazionale e sistemi di tipo, potete trovare esercizi (spesso risolti) sul libro di Pierce
  • su asserzioni alla Hoare, potete trovare esercizi d'esame di questo tipo come prove intemedie o parti di testi d'esame del corso di MFI, riportate qui:



Ritorno alla pagina precedente

Per suggerimenti e commenti si prega di scrivere a:
Elena Zucca zucca@disi.unige.it

Ultima modifica: 18 agosto 2011