COQ introductory mini-course

COQ introductory mini-course
Andrea Masini (Università di Verona)

Program
1) Recalls of natural deduction (classical and intuitionist) and of typed lambda calculus.
2) Examples of simple proofs in Coq (Goal, Assumptions and Tactics).
3) Functional programming in CoQ.
4) Structured data types.
5) Polymorphism and higher order functions.
6) The basic tactics.
7) Logic in CoQ.
8) Induction

Unfortunately, in a course of only 12 hours, even if intensive, it will not be possible to tackle the applications of COQ, which range from the specification and proof of properties of complex computer systems (SW and HW) to the mechanisation of mathematics (continuous and discrete).

Timetable
Wednesday 9 September 2020, at [10.00-13.00]
Thursday 10 September 2020, at [10.00-13.00]
Wednesday 16 September 2020, at [10.00-13.00]
Thursday 17 September 2020, at [10.00-13.00]

The course is open to everyone, the only pre-requisite is to have the basic knowledge of logic.

It is still not clear whether the course will be held in presence or on-line. We’re waiting for precise indications from the doctoral school.