Friday, July 9th
Friday's program is also available with abstracts and side by side with other events.
08:50‑10:00 Opening. Invited Talk
Location: IF 4.31+4.33
| 08:50 | Opening |
| 09:00 | Gerard Berry (INRIA, College de France) What could be the right balance between abstract and fine-grain computational properties? |
10:30‑11:30 Invited tutorial
Location: IF 4.31+4.33
| 10:30 | Dan Ghica (University of Birmingham) Geometry of Synthesis: Semantics-directed hardware compilation |
11:30‑12:30 Session 1
Location: IF 4.31+4.33
| 11:30 | Magnus O. Myreen and Michael J. C. Gordon Machine code: architecture-independent formal verification and proof-producing compilation |
| 12:00 | Ugo Dal Lago On the Role of Interaction in Implicit Computational Complexity |
14:00‑15:00 Invited talk
Location: IF 4.31+4.33
| 14:00 | Alex Simpson (LFCS, University of Edinburgh) Linear types for continuations |
15:30‑16:30 Session 2
Location: IF 4.31+4.33
| 15:30 | Nick Benton and Chung-kil Hur Step-Indexing: The Good, the Bad and the Ugly |
| 15:50 | Guilhem Jaber and Nicolas Tabareau Krivine realizability for compiler correctness |
| 16:10 | Shin-ya Katsumata and Rasmus Møgelberg Fullness of monadic translation by TT-lifting |
16:30‑17:00 Panel Discussion
Location: IF 4.31+4.33
17:00‑18:00 Session 3
Location: IF 4.31+4.33
| 17:00 | Rasmus Ejlers Møgelberg and Sam Staton Full abstraction in a metalanguage for state |
| 17:20 | Antoine Madet, Roberto M. Amadio and Patrick Baillot An Affine-Intuitionistic System of Types and Effects: Confluence and Termination |
| 17:40 | Nathaniel Charlton and Bernhard Reus A deeper understanding of the deep frame axiom (extended abstract) |