| Organizer: | Lars Birkedal, Room 4C 15, 7218 5280 |
This is a Ph.D.-seminar in which we study some aspects of semantics of programming langauges and type theories relevant to computer science. This semester we focus on recent models of Separation Logic and Hoare Type Theory and on recent methods for proving contextual equivalence for languages with higher-types and general references. We'll cover the necessary background material. Basic knowledge of denotational semantics and introductory category theory is assumed.
Readings will include (excerpts from some of):
Wish list (possible future topics):
Meeting time: We meet on Wednesday, 10:00--12:00, Room 3A-01 (except Nov. 8: 2A-05), starting Sep. 27.
Schedule:
| Date | Speaker | Reading | ||
|---|---|---|---|---|
| Wed | Sep | 27 | LB | Categories of cpo's I |
| Wed | Oct | 04 | BB | Adequacy for CBV and CBN PCF |
| Wed | Oct | 11 | BB | Hyperdoctrines |
| Wed | Oct | 18 | Fall Break | |
| Wed | Oct | 25 | NB | Recursive Domains and Adequacy |
| Wed | Nov | 01 | AF | Recursive Domains and Effects |
| Wed | Nov | 08 | LB | Separation Logic / BI / BI hyperdoctrines |
| Wed | Nov | 15 | LB | Models for Idealized ML |
| Wed | Nov | 22 | LB | Models for Idealized ML |
| Fri | Nov | 29 | NB | Logical relations for state |
| Wed | Dec | 06 | LB / RLP | Categorical Models of DTT |
| Wed | Dec | 13 | BB | Models of FHoDTT, Pers and Assemblies |
| Wed | Dec | 20 | LB | Models of Hoare Type Theory, HTTHOL |