Studying at the University of Verona

Here you can find information on the organisational aspects of the Programme, lecture timetables, learning activities and useful contact details for your time at the University, from enrolment to graduation.

This information is intended exclusively for students already enrolled in this course.
If you are a new student interested in enrolling, you can find information about the course of study on the course page:

Laurea magistrale in Ingegneria e scienze informatiche - Enrollment from 2025/2026

The Study Plan includes all modules, teaching and learning activities that each student will need to undertake during their time at the University.
Please select your Study Plan based on your enrollment year.

CURRICULUM TIPO:

1° Year 

ModulesCreditsTAFSSD
12
B
ING-INF/05
12
B
ING-INF/05
6
B
ING-INF/05

2° Year   activated in the A.Y. 2020/2021

ModulesCreditsTAFSSD
6
B
ING-INF/05
6
B
INF/01
Other activities
4
F
-
Final exam
24
E
-
ModulesCreditsTAFSSD
12
B
ING-INF/05
12
B
ING-INF/05
6
B
ING-INF/05
activated in the A.Y. 2020/2021
ModulesCreditsTAFSSD
6
B
ING-INF/05
6
B
INF/01
Other activities
4
F
-
Final exam
24
E
-
Modules Credits TAF SSD
Between the years: 1°- 2°

Legend | Type of training activity (TTA)

TAF (Type of Educational Activity) All courses and activities are classified into different types of educational activities, indicated by a letter.




S Placements in companies, public or private institutions and professional associations

Teaching code

4S02789

Credits

6

Language

Italian

Scientific Disciplinary Sector (SSD)

INF/01 - INFORMATICS

Period

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

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.

Reference texts
Author Title Publishing house Year ISBN Notes
Carl A. Gunter Semantics of Programming Languages MIT Press 1992 0262570955
Peter Sewell Semantics of Programming Languages (Edizione 6) Cambridge University Press 2019
G. Winskel The formal Semantics of Programming Languages MIT Press 1993
Benjamin Pierce Types and Programming Languages (Edizione 1) MIT Press 2002 ISBN-10: 0262162091

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.

Students with disabilities or specific learning disorders (SLD), who intend to request the adaptation of the exam, must follow the instructions given HERE