Preliminary Programme
1st Day, 28 Nov | 2nd Day, 29 Nov | 3rd Day, 30 Nov | 4th Day, 1 Dec
| 27 November (Saturday) | |
| 10:00-20:00 | Registration (Hengshan Hotel) |
| 28 November (Sunday) | |
| 9:00-14:00 | Registration (Hengshan Hotel) |
| 14:30-16:00 | Tutorial I: Probabilistic testing semantics Yuxin Deng |
| 16:00-16:30 | Coffee break | 16:30-18:00 | Tutorial II: A Logical Mix of Approximation and Separation Aquinas Hobor and Robert Dockins |
| 18:30 - 20:30 | Reception |
| 29 November (Monday) | |
| 9:00-9:15 | Opening |
| 9:15-10:15 |
Keynote Address (Session Chair: Kazunori Ueda) A Calculus for Hybrid CSP ZHOU Chaochen |
| 10:15-10:45 | Coffee break | 10:45-12:15 | Session 1 (Session Chair: Sungwoo Park) Typechecking Higher-Order Security Libraries Karthikeyan Bhargavan, Cedric Fournet and Nataliya Guts Deriving Type Systems and Implementations for Coroutines Konrad Anton and Peter Thiemann Liberal Typing for Functional Logic Programs Francisco J. Lo'pez-Fraguas, Enrique Martin-Martin and Juan Rodriguez-Hortala |
| 12:15 - 13:45 | Lunch break | 13:45-15:15 | Session 2 (Session Chair: Zhenjiang Hu) A Provably Correct Stackless Intermediate Representation for Java Bytecode Delphine Demange, Thomas Jensen and David Pichardie JNI Light: An Operational Model for the Core JNI Gang Tan An interactive tool for analyzing embedded SQL queries [system and tool presentation] Aivar Annamaa, Andrey Breslav, Jevgeni Kabanov and Varmo Vene |
| 15:15-15:45 | Coffee break | 15:45-16:45 |
Invited talk 1 (Session Chair: Yuxi Fu) Foundations of Quantum Programming Mingsheng Ying |
| 16:45-17:00 | Short break | 17:00-18:00 | Session 3 (Session Chair: Kwangkeun Yi) Simple and Precise Widenings for H-Polyhedra Axel Simon and Liqian Chen Metric Spaces and Termination Analyses Aziem Chawdhary and Hongseok Yang |
| 30 November (Tuesday) | |
| 9:00-10:00 |
Invited Talk 2 (Session Chair: Alwen Tiu) From a Verified Kernel Towards Verified Systems Gerwin Klein |
| 10:00-10:30 | Coffee break | 10:30-12:00 | Session 4 (Session Chair: Peter Thiemann) Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics Jan Hoffmann and Martin Hofmann Interprocedural Control Flow Reconstruction Andrea Flexeder, Helmut Seidl, Michael Petter and Bogdan Mihaila Data Structure Fusion Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard and Mooly Sagiv |
| 12:00 - 13:30 | Lunch break | 13:30-15:00 | Session 5 (Session Chair: Jacques Garrigue) Categorical Descriptional Composition Shin-ya Katsumata Bisimulation proof methods in a path-based specification language for polynomial coalgebras Xiaocong Zhou, Yongji Li, Wenjun Li, Haiyan Qiao and Zhongmei Shu Context-Preserving XQuery Fusion Hiroyuki Kato, Soichiro Hidaka, Zhenjiang Hu, Keisuke Nakano and Yasunori Ishihara |
| 15:00-15:30 | Coffee break |
| 15:30-16:15 | Poster Session (Chair: Guoqiang Li) | 16:15-17:15 | Session 6 (Session Chair: Hideya Iwasaki) Index-Compact Garbage Collection Liangliang Tong and Francis C.M. Lau Live heap space bounds for real-time systems Martin Kero, Pawel Pietrzak and Johan Nordlander |
| 18:00 - 20:30 | Banquet |
| 1 December (Wednesday) | |
| 9:00-10:00 |
Invited Talk 3 (Session Chair: Sungwoo Park) Reasoning about Computations Using Two-Levels of Logic Dale Miller |
| 10:00-10:30 | Coffee break | 10:30-12:00 | Session 7 (Session Chair: Aquinas Hobor) A Quick Tour of the VeriFast Program Verifier [system and tool presentation] Bart Jacobs, Jan Smans and Frank Piessens Verification of Tree-Processing Programs via Higher-Order Model Checking Hiroshi Unno, Naoshi Tabuchi and Naoki Kobayashi Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates Soonho Kong, Yungbum Jung, Cristina David, Bow-yaw Wang and Kwangkeun Yi |
| 12:00 - 13:30 | Lunch break | 13:30-15:00 | Session 8 (Session Chair: Tyng-Ruey Chuang) Relational Parametricity for a Polymorphic Linear Lambda Calculus Jianzhou Zhao, Qi Zhang and Steve Zdancewic A Certified Implementation of ML with Structural Polymorphism Jacques Garrigue Type Inference for Sublinear Space Functional Programming Ugo Dal Lago and Ulrich Schoepp |
| 15:00-15:30 | Coffee break | 15:30-17:00 | Session 9 (Session Chair: Yuxin Deng) Liveness of Communicating Transactions (Extended Abstract) Edsko de Vries, Vasileios Koutavas and Matthew Hennessy Model Independent Order Relations for Processes Chaodong He Concurrency Can't Be Observed, Asynchronously Paolo Baldan, Filippo Bonchi, Fabio Gadducci and Giacoma Monreale |
1st Day, 28 Nov | 2nd Day, 29 Nov | 3rd Day, 30 Nov | 4th Day, 1 Dec