Laurea e Diploma in Informatica

 Page under construction

Corso di Metodi Formali dell'Informatica - a.a. 1999/00

• Ultima modifica: 23 Ottobre 1999
• Docente: Prof. Eugenio Moggi (email moggi@disi.unige.it)
• Orario (I semestre): Mar 14-15, Mer 9-11, Ven 11-13 (Aula 710) - inizio Mercoledi' 03/11/1999
  Orario (II semestre): Lun 10-13, Ven 11-13 (Aula 710) - inizio Lunedi' 06/03/2000
• Informazioni generali: Prerequisiti, Obiettivi, Programma, Testi di Riferimento
• Informazioni on line: registro delle lezioni, note,
• Lista degli studenti
• ESAMI: situazione voti, Testi e soluzioni di esami precedenti
• Risultati Compitini 11/01/2000, 20/03/2000, 28/04/2000, 02/06/2000

Prerequisiti

Obiettivi

Modalita' degli esami

Programma

• preliminari matematici (10h):
  • definizioni induttive e principi di induzione
  • segnature, termini, algebre ed interpretazioni
  • nozioni elementari di teoria delle categorie
• semantica dei linguaggi di programmazione (36h):
  • sintassi e semantica operazionale di IMP (while language)
  • semantica denotazionale di IMP
  • semantica assiomatica di IMP: Hoare's triples
  • relazioni tra le semantiche di IMP
  • domini e definizioni ricorsive, costruzioni di domini
  • lambda calcolo come metalinguaggio
  • sintassi e semantica di HOFL (functional language)
  • osservazioni ed adeguatezza, soundness, equivalenza osservazionale e full abstraction
• specifiche algebriche (12h):
  • specifiche del primo ordine e modelli (semantica loose)
  • sistemi deduttivi soundness e completeness (relativamente ad un frammento)
  • modello iniziale (semantica inziale)
  • specifiche condizionali ed esistenza del modello iniziale
  • specifiche equazionali e sistemi di riscrittura
  • confluenza, terminazione, forme normali
  • coppie critiche, sistemi ortogonali
• sistemi di tipo (12h):
  • semantica operazionale del lambda calcolo con costanti
  • tipaggio ed analisi statica
  • realizzabilita' (pCA) e semantica dei tipi (PER)
  • polimorfismo
  • type inference (algoritmo di Hindley-Milner)
• semantica per i sistemi concorrenti (12h):
  • sistemi di transizione etichettati (LTS)
  • CCS: sintassi, semantica operazionale, LTS dei processi
  • equivalenze per LTS: trace equivalence, strong e weak bisimulation
  • proprieta' di un LTS: logica di Hennessy-Milner

Testi di Riferimento

• *[Acz77] P.Aczel. An Introduction to Inductive Definitions. Handbook of Mathematical Logic, J.Barwise (ed), North-Holland, 1977. [Pag. 739-745]
• [Car97] L.Cardelli. Type Systems. Handbook of Comp. Sci. and Engineering, CRC Press, 1997.
• [HS86] J.R.Hindley, J.P.Seldin. Introduction to Combinators and Lambda-Calculus. Cambridge University Press, 1986. (CH 1-3, 6-10)
• [Klo92] J.W.Klop. Term Rewriting Systems. In Vol. 2 of Handbook of Logic in Computer Science (Abramsky et. al. eds). Oxford Univ. Press, 1992.
• [Mil89] R.Milner. Communication and Concurrency. Prentice Hall International, 1989.
• [Mit90] J.C.Mitchell. Type Systems for Programming Languages. In Handbook of Theoretical Computer Science (van Leeuwen ed). MIT Press, 1990.
• [Mit96] J.C.Mitchell. Foundations for Programming Languages. MIT Press, 1996.
• *[Pie91] B.C.Pierce. Basic Category Theory for Computer Scientists. MIT Press, 1991. [Ch 1]
• *[Ten91] R.D.Tennent. Semantics of Programming Languages. Prentice Hall International, 1991. [Ch 8]
• *[Win93] G.Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993. [Ch 1-5, 8, 11]
  VEDI http://www.amazon.com PER L'ACQUISTO (la versione paperback si intitola "Formal Semantics")