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 29th April 2024 on a date agreed between the student and the
lecturer
Tutorial meeting :
via Zoom
(please send me an email with your request).
Please just use your academic email address.
P. Martin-Loef
Intuitionistic type theory.
Notes by G. Sambin of a series of lectures given in Padua, June 1980, Bibliopolis 1984.
For further reading:
"La teoria dei tipi"
in "Direzioni della ricerca logica in Italia 2", ETS, eds. H.Hosni, G. Lolli, C. Toffalori (in Italian)
P. Wadler's textbook ``Programming Language Foundations in Agda" as a literate script in Agda freely available with a paper presentation here
(for computer scientists)