Teaching code

4S02789

Teacher

Massimo Merro

Credits

6

Language

Italian

Scientific Disciplinary Sector (SSD)

INF/01 - INFORMATICS

Period

I semestre dal Oct 1, 2019 al Jan 31, 2020.

Lessons timetable Moodle Seminars

To show the organization of the course that includes this module, follow this link:  Course organization

Learning outcomes

The course aims to provide the theoretical foundations of programming languages ​​belonging to three different programming paradigms: imperative, functional and concurrent. In particular, techniques are provided for the definition of formal semantics and tools for analyzing programs at compile time.

At the end of the course, the student will be able to formally define a new programming language, also in a research context, through a formal operational semantics and type systems for a static analysis of the correctness of the programs written in the language.

This knowledge will allow the student to: i) formally test the propriety of an arbitrary semantics using different techniques of induction; ii) formally test the correctness of a type system; iii) master semantic behavioral equivalences to compare the dynamic behavior of two different programs.

At the end of the course, the student will be able: i) to compare different languages ​​and choose between them the most appropriate according to the context of use and to make the most appropriate design choices when defining a new language; ii) to continue independently his/her studies in the field of programming languages ​​and software development independently.

Program

Classes and exercises (56 hours)

• 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 subtying 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.

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 4 or 5 exercises. The correct conduct of all exercises allows for a 30/30 vote.