| 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. Last semester we covered most of the necessary background material
Readings will include (excerpts from some of):
To do:
To gain credit for this 7 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 Wednesday, 10:00--12:00, Room 3A 01. starting Feb. 07, 2007.
Tentative Schedule:
| Date | Speaker | Reading | ||
|---|---|---|---|---|
| Wed | Feb | 07 | LB | Intro + Idealized ML |
| Wed | Feb | 14 | JT | Paul Blain Levy: Possible World .... |
| Wed | Feb | 21 | LB | Kripke model, realizability style (recall Pitts' relational properties of domains article from last semester and see LB notes circulated by email) |
| Wed | Feb | 28 | LB | continuation of last week |
| Wed | Mar | 07 | KS | Appel et. al. |
| Wed | Mar | 14 | KS | Appel et. al. |
| Wed | Mar | 21 | LB / JT | Birkedal and Yang: Relational Parametricity and Separation Logic |
| Wed | Apr | 04 | Cancelled (Easter break) | |
| Wed | Apr | 11 | B. Reus | Reus + Schwinghammer: Sep. Logic for higher-order store |
| Wed | Apr | 18 | KS | Inductive Reasoning about Effectful Data Types |
| Wed | Apr | 25 | LB | Relational Reasoning for Recursive Types and References |
| Wed | May | 2 | LB | Nanevski et. al.: Hoare Type Theory |
| Wed | May | 9 | LB | Nanevski et. al.:Hoare Type Theory |
| Wed | Mar | 16 | JT | Shinwell: FM-domain theory |