| Organizers: | Lars Birkedal, birkedal@itu.dk, Room 2.21, 3816 8868 | Carsten Butz, butz@itu.dk, Room 1.17, 3816 8820 |
This is a Ph.D. seminar in which we study aspects of topos theory relevant to computer science. After having read material from Peter Johnstone's opus: Sketches of an Elephant: A Topos Theory Compendium we plan to pause and read parts of
To gain credit for this 7.5 ECTS seminar you have to participate actively in the discussions. Moreover, you have to take responsibility for at least one topic, stretching usually over more than a week.
Meeting time: We meet on Fridays, 14:00--15:30, Room 2.55.
Participants:
Schedule:
| Date | Speaker | Reading | ||
|---|---|---|---|---|
| Fri | Aug | 29 | CB | Introduction |
| Fri | Sep | 5 | - | No meeting |
| Fri | Sep | 12 | A: NTS | I.1 - I.6: Propositional calculus, deductive systems, cartesian closed categories |
| Fri | Sep | 19 | A: NTS | Continued |
| Fri | Sep | 26 | B: CB | I.8 - I.11: CCCs with coproducts, typed lambda calculus, relation between the two |
| Fri | Oct | 3 | B: CB | Continued |
| Fri | Oct | 10 | C: CB | II.1, II.2: Type theories |
| Fri | Oct | 17 | - | No meeting |
| Fri | Oct | 24 | D: RM | II.3, II.4: Internal logic of a topos, Peano's axioms |
| Fri | Oct | 31 | D: RM | II.5, II.6: The internal logic at work |
| Fri | Nov | 7 | E: MB | II.7: Choice, Boolean toposes (plus suplemental material) |
| Fri | Nov | 14 | F: BB | II.8, II.9: Topos semantics |
| Fri | Nov | 21 | F: BB | Continued |
| Fri | Nov | 28 | H: RLP | II.11 - II.14: Toposes and type theories (selection) |
| Fri | Dec | 5 | G: MB | II.10: Sheaves |
| Fri | Dec | 12 | I: VS | II.18: Sheaf representation |
| Fri | Dec | 19 | J: RLP | II.20, II.21: Intuitionistic principles |