Teaching code

4S008895

Credits

12

Coordinator

Massimo Merro

Language

Italian

Scientific Disciplinary Sector (SSD)

ING-INF/05 - INFORMATION PROCESSING SYSTEMS

Moodle Seminars 0

The teaching is organized as follows:

Learning outcomes

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.

Program

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. Rule-based inductive definitions and proofs. Proofs of type safety properties. Exercises.

• Functions. Call-by-name and call-by-value 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 non-equivalence. Exercises.

• Concurrency. Shared variable interleaving. Semantics for simple mutexes; a serializability property. Semantic equivalence for concurrent languages. Exercises.

Second part.

• Order, lattices, relations, fix-point 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.

Bibliography

Examination Methods

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 rule-based);
• to be familiar with some operationally-based 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.