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.
Study Plan
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/2026The 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.
1° Year
Modules | Credits | TAF | SSD |
---|
2° Year activated in the A.Y. 2020/2021
Modules | Credits | TAF | SSD |
---|
Modules | Credits | TAF | SSD |
---|
Modules | Credits | TAF | SSD |
---|
Modules | Credits | TAF | SSD |
---|
2 modules among the following
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.
Foundations of Computing - LINGUAGGI (2019/2020)
Teaching code
4S02789
Teacher
Credits
6
Language
Italian
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
Period
I semestre dal Oct 1, 2019 al Jan 31, 2020.
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.
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.