INFO on the final examination:
oral examination consisting in solving exercises on the theory part on paper and exercises via the proof-assistant Agda before hand
on a date agreed between the student and the lecturer.
The candidate can decide to pass the exam by choosing to privilege either the theory part or the computer-aided formalization part
Exam giving privilege to the theory part : the candidate is required to solve about 8 exercises from the theory syllabus agreed with the lecturer and only 1 or 2 exercises in Agda agreed with the lecturer
Exam giving privilege to the computer-aided formalization part: the candidate is required to solve about 4 exercises from the theory syllabus agreed with theory lecturer and a formalization project in Agda agreed with the Agda lecturer
Partial examinations are possible (either on the theory part only or on the formalization project only) after Easter 2025 on a date agreed between the student and the lecturer
