6 EC
Semester 2, period 5
5314TYTH6Y
| Owner | Master Logic |
| Coordinator | B. van den Berg |
| Part of | Master Logic, |
Type theory is a subject which lies at the intersection of mathematics, logic and computer science. In this course the emphasis will be on how type theory can be used as a framework for developing mathematics and verifying mathematical proofs. We will discuss various version of the lambda calculus (untyped, simply typed, second order typed and dependently typed). The course will culminate in the Calculus of Constructions (CoC) and investigate how that provides a setting for formalising mathematics.
Rob Nederpelt and Herman Geuvers, Type theory and formal proof - an introduction, Cambridge University Press 2014.
|
Activity |
Hours |
|
|
Hoorcollege |
28 |
|
|
Tentamen |
3 |
|
|
Werkcollege |
14 |
|
|
Self study |
123 |
|
|
Total |
168 |
(6 EC x 28 uur) |
This programme does not have requirements concerning attendance (TER-B).
| Item and weight | Details |
|
Final grade | |
|
Tentamen | Must be ≥ 5 |
|
Homework | |
|
Final grade after retake | |
|
Hertentamen | Must be ≥ 5 |
|
Homework |
Homework counts for 30%, while the exam counts for 70%.
The 'Regulations governing fraud and plagiarism for UvA students' applies to this course. This will be monitored carefully. Upon suspicion of fraud or plagiarism the Examinations Board of the programme will be informed. For the 'Regulations governing fraud and plagiarism for UvA students' see: www.student.uva.nl
| Weeknummer | Onderwerpen | Studiestof |
| 1 | ||
| 2 | ||
| 3 | ||
| 4 | ||
| 5 | ||
| 6 | ||
| 7 | ||
| 8 |
The schedule for this course is published on DataNose.
There will be a Canvas page for the course.