Host: Philippa Gardner
Studio A, Huxley Building, Imperial ( Map ).
If coming from South Kensington (easiest to explain from map), go to Huxley Building along the main walkway (clearly marked). Get to the door of Huxley, don't go in, but instead follow signs to Studio A/B (turn right, doubling back on yourself).
09:30 Coffee/tea and Welcome
10:00 Keynote Talk. Andrew Appel (Princeton & INRIA Roquencourt). Toward Separation Logic Correctness Proofs of Concurrent C Programs
11:00 Break
11:30 Dino Distefano (Queen Mary). Automatic Termination Proofs for Programs with Shape-Shifting Heaps
12:00 Philippa Gardner (Imperial). Separation Logic v First-order Logic: Parametric Inexpressivity Results
12:30 Lunch
14:00 Sophia Drossopoulou (Imperial, ETAPS Invited Talk). Types for Hierarchy Shapes
14:45 Sebastian Hunt (City). Flow-Sensitive Security Types
15:15 Break
15:45 Paulo Oliva (Queen Mary). Generalized Hoare Logic
16:15 Danielle Varacca (Imperial). A topological characterisation of fairness