| 08:30-10:00 | Session I: Program Specification |
| Invited talk I: Towards a Program Logic for JavaScript | |
| Philippa Gardner (Imperial College) | |
| [Abstract] [Slides] | |
| TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs | |
| Radu Grigore, Rasmus Lerchedahl Petersen and Dino Distefano | |
| [Abstract] [Full paper] [Slides] | |
| 10:00-10:30 | coffee break |
| 10:30-12:00 | Session II: Models and Types |
| An automata-theoretic model of objects | |
| Uday Reddy and Brian Dunphy | |
| [Abstract] [Full paper] [Slides] | |
| Information Flow Control with Errors | |
| Andreas Gampe and Jeffery Von Ronne | |
| [Abstract] [Full paper] [Slides] | |
| Types for Precise Thread Interference | |
| Jaeheon Yi, Tim Disney, Stephen Freund and Cormac Flanagan | |
| [Abstract] [Full paper] [Slides] | |
| 12:00-14:00 | lunch |
| 14:00-15:30 | Session III: Virtual Components |
| Invited talk II: Virtual Extension Methods for Java | |
| Alex Buckley and Brian Goetz (Oracle) | |
| [Abstract] [Slides] | |
| Reduction and typing of class definitions with complex content | |
| Peter Vanderbilt | |
| [Abstract] [Full paper] [Slides] | |
| 15:30-16:00 | coffee break |
| 16:00-17:00 | Session IV: Mechanical Proofs and Empirical Studies |
| Proving the Correctness of Fractional Permissions for a Java-like Kernel Language | |
| John Boyland and Chao Sun | |
| [Abstract] [Full paper] [Slides] | |
| An Empirical Study on the Rewritability of the with Statement in JavaScript | |
| Changhee Park, Hongki Lee and Sukyoung Ryu | |
| [Abstract] [Full paper] [Slides] |