Work Plan for Week 1

To get started, make sure to do the following:

• install Coq (see the instructions),
• familiarise yourself with the course (see the home page), and
• join the Mattermost team for this course.

Material

name	file name	short version	note
Preface	Preface.html		you can ignore the information about course management, which does not apply to us
Functional Programming in Coq	Basics[.html|.v]	download
Proof by Induction	Induction[.html|.v]	download

Schedule

date	time	location	type
Monday, 1 September	15:45 - 17:45	Aula - Hall C	lecture
Tuesday, 2 September	8:45 - 10:45	CEG - Hall D	lecture
Thursday, 4 September	13:45 - 15:45	Pulse - Hall 2 & 3	problem session

Problem Session

file	exercises
Basics[.html|.v]	andb_true_elim2
Induction[.html|.v]	all exercises from the “Proof by Induction” section (starting at mul_0_r and ending with even_S)

---

If you need help, make a request during the problem session in the Queue or reach out on Mattermost.