An Introduction to Interactive Theorem Proving (2022)

Description:
This course will be a hands-on course about interactive theorem proving. We will use a proof assistant to construct formal models of algorithms, protocols, and programming languages and to reason about and verify their properties. Proof assistants, like Coq or Isabelle, are tools that mechanically check human-written proofs, while assisting their users in constructing these proofs. This course will be centered around the Isabelle proof assistant. The course interleaves the introduction of various modeling and proof techniques with exercises in which students apply these techniques.

Prerequisites:
Basic mathematics, functional programming and formal semantics at the level taught for BSc/MSc students in computer Science.

Organizer: Professor (MSO) Bent Thomsen

Lecturers: Dmitriy Traytel (KU), Anders Schlichtkrull (AAU), René Rydhof Hansen (AAU)

ECTS: 2.0

Time: 16-17 May 2022, at 08.00 - 16.00

Place: room 02.90, SLV 300

Number of seats: 30

Deadline: 18 April 2022

Important information concerning PhD courses:
We have over some time experienced problems with no-show for both project and general courses. It has now reached a point where we are forced to take action. Therefore, the Doctoral School has decided to introduce a no-show fee of DKK 3.000 for each course where the student does not show up. Cancellations are accepted no later than 2 weeks before start of the course. Registered illness is of course an acceptable reason for not showing up on those days. Furthermore, all courses open for registration approximately four months before start. This can hopefully also provide new students a chance to register for courses during the year. We look forward to your registrations.