Foundations of programming and specification languages (2020/2021)



Course code
4S008895
Credits
12
Coordinator
Massimo Merro
Academic sector
ING-INF/05 - INFORMATION PROCESSING SYSTEMS
Language of instruction
Italian
Teaching is organised as follows:
Activity Credits Period Academic staff Timetable
Teoria 10 I semestre Maria Paola Bonacina, Massimo Merro

Go to lesson schedule

Laboratorio 2 I semestre Massimo Merro

Go to lesson schedule

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.

Syllabus

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.

Assessment methods and criteria

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.

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