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 |
|---|
4 modules among the following2° Year It will be activated in the A.Y. 2025/2026
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
4 modules among the following| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
3 modules among the following2 modules among the followingLegend | 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.
Interactive Theorem Proving (2024/2025)
Teaching code
4S010508
Teacher
Coordinator
Credits
6
Language
Italian
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
Period
Semester 1 dal Oct 1, 2024 al Jan 31, 2025.
Courses Single
Authorized
Learning objectives
The aim of the course is to provide an introduction to the techniques of mechanization of logical reasoning, using tools based on automatic deduction systems or proof assistant systems. Particular importance will be given to the techniques of formalization and mechanical reasoning using goal-driven software systems. At the end of the course students will be able to deal with formalization and automatic verification using either automatic reasoners or proof-assistants. Students will be able to continue their studies in the field of mechanical reasoning, for example by developing master's theses.
Prerequisites and basic notions
Basics of logic
Program
Part 1- Foundations
Recalls of natural deduction (classical and intuitionistic)
Simple typed Lambda calculus.
Type checking and type inference.
The system F and the Calculus of Constructions.
Introduction to automatic deduction in propositional logic.
Part 2 - The Coq system
Simple proofs in Coq (Goal, assumptions and tactics).
Functional programming in CoQ.
Structured data types.
Polymorphism and higher order functions.
The tactics.
Logic in CoQ.
Induction and co-induction.
Bibliography
Didactic methods
Frontal and interactive lessons.
Learning assessment procedures
Students will be assigned a project to be completed in one month from the first exam session. Each project can be carried out by a group of one or two people. The project must be written in Coq (with the code adequately commented) and be accompanied by a report of a few pages. Each project can be created using the constructs and tactics seen in class. Every construct and tactic used and not explained in class must be explained in the accompanying report. The exam will consist of an oral test in which the project carried out will be discussed. Students with disabilities or specific learning disorders (DSA), who intend to request the adaptation of the exam, must follow the instructions given
Evaluation criteria
The following will be evaluated: 1) the implementation of the project; 2) the oral exam in which the project is discussed.
Criteria for the composition of the final grade
The final grade will be based on how the project was carried out and on how the examinees answer the questions during the oral exam.
Exam language
Italiano e inglese
