Teaching is organised as follows:  
Activity  Credits  Period  Academic staff 
Teoria  10  I semestre 
Maria Paola Bonacina
Massimo Merro 
Laboratorio  2  I semestre 
Massimo Merro

The course aims at providing the theoretical basis of programming languages belonging to three different programming paradigms: imperative, functional and concurrent. In particular, the following issues are addressed: (i) techniques for the definition of formal syntax and semantics, (ii) logics for expressing formal properties of good behavior of programs, (iii) tools for static analysis of programs, (iv ) notions of behavioral equivalences between programs. At the end of the course, the student will be able to formally define a new programming language, also in a research context, through syntax, formal semantics and type systems for the static analysis of the correctness of programs written in the language. It will also be able to express programs' good behavior properties through logical languages. This knowledge will allow the student to: i) formally prove correctness properties of an arbitrary semantics using different induction techniques; ii) formally prove if a program satisfies a certain good behavior property; iii) formally prove the correctness of a type system; iv) master semantic behavioral equivalences in order to compare the behavior, at run time, of two different programs. At the end of the course, the student will be able to: i) compare different languages and choose the most suitable one according to the context of use and make the most appropriate design choices when defining a new language; ii) continue studies in the programming languages and software development independently.
First part.
• Introduction. Transition systems. The idea of structural operational semantics. Transition semantics of a simple imperative language. Language design options. Exercises.
• Types. Introduction to formal type systems. Typing for the simple imperative language. Statements of desirable properties.
• Induction. Review of mathematical induction. Abstract syntax trees and structural induction. Rulebased inductive definitions and proofs. Proofs of type safety properties. Exercises.
• Functions. Callbyname and callbyvalue function application, semantics and typing. Local recursive definitions. Exercises.
• Data. Semantics and typing for products, sums, records, references. Exercises.
• Subtyping. Record subtyping, function subtyping and simple object encoding. Exercises.
• Semantic equivalence. Semantic equivalence of phrases in a simple imperative language, including the congruence property. Examples of equivalence and nonequivalence. Exercises.
• Concurrency. Shared variable interleaving. Semantics for simple mutexes; a serializability property. Semantic equivalence for concurrent languages. Exercises.
Second part.
• Order, lattices, relations, fixpoint theorems. Exercises.
• Denotational Semantics of an imperative language. Exercises.
• Program properties and specification languages (examples). Exercises.
• Hoare Logic (completeness & incompleteness of Hoare Logic), partial/total correctness. Exercises.
• Decidability, safety, liveness, security. Exercises.
• Trace semantics — Kripke structures. Exercises.
• Elements of Temporal Logic. Exercises.
To pass the exam the student must show:
• to be able to define the operational semantics and type systems for some simple imperative, functional and interactive program language;
• to be able to prove properties of an operational semantics using various forms of induction (mathematical, structural, and rulebased);
• to be familiar with some operationallybased notions of semantic equivalence of program phrases and their basic properties.
The exam consists of a written test containing 3 exercises. The correct conduct of all exercises allows for a 30/30 vote.
Reference books  
Activity  Author  Title  Publisher  Year  ISBN  Note 
Teoria  Dovier A. Giacobazzi R.  Fondamenti dell'Informatica: Linguaggi Formali, CalcolabilitÃ e ComplessitÃ .  Bollati Boringhieri  2020  9788833933795  
Teoria  Peter Sewell  Semantics of Programming Languages (Edizione 6)  Cambridge University Press  2019  
Teoria  Aaron R. Bradley, Zohar Manna  The Calculus of Computation  Decision Procedures with Applications to Verification (Edizione 1)  Springer  2007  9783540741  
Teoria  G. Winskel  The formal Semantics of Programming Languages  MIT Press  1993 
© 2002  2021
Verona University
Via dell'Artigliere 8, 37129 Verona 
P. I.V.A. 01541040232 
C. FISCALE 93009870234