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
2° Year activated in the A.Y. 2023/2024
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
4 modules among the following2 modules among the following3 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 (2022/2023)
Teaching code
4S010508
Teacher
Coordinator
Credits
6
Language
Italian
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
Period
Semester 2 dal Mar 6, 2023 al Jun 16, 2023.
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.
Didactic methods
Frontal and interactive lessons.
Learning assessment procedures
To pass the exam, a project must be carried out which will be awarded one month before the first exam. Each project can be carried out by a group of one or two people. The project must be written in Coq (with the code properly commented) and be accompanied by a report of a few pages. Each project can be made using the constructs and tactics seen in class. Any construct and tactics used and not explained in class must be explained in the accompanying report. The exam will consist of an oral exam in which the project carried out will be discussed.
Evaluation criteria
The following will be evaluated:
1) the realization of the project;
2) the oral 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 examiners will answer the questions during the oral session.
Exam language
Italiano
