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.
M.H. Soerensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006.
|
Activity |
Hours |
|
|
Hoorcollege |
28 |
|
|
Tentamen |
3 |
|
|
Werkcollege |
28 |
|
|
Self study |
109 |
|
|
Total |
168 |
(6 EC x 28 uur) |
This programme does not have requirements concerning attendance (TER-B).
| Item and weight | Details |
|
Final grade | |
|
70% Tentamen | |
|
30% Homework | |
|
1 (20%) Homework sheet 1 | |
|
1 (20%) Homework sheet 2 | |
|
1 (20%) Homework sheet 4 | |
|
1 (20%) Homework sheet 3 | |
|
1 (20%) Homework sheet 5 |
The grade will be based on 5 homework assignments, which together count for 30%, and a final written exam, which counts for 70%. The grade for the retake is calculated in the same way.
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.