## Accepted Papers

**Manifest Contracts with Intersection Types**

Yuki Nishida (Kyoto University), Atsushi Igarashi (Kyoto University)

**A Dependently Typed Multi-Stage Calculus**

Akira Kawata (Kyoto University), Atsushi Igarashi (Kyoto University)

**Existential Types for Relaxed Noninterference**

Raimil Cruz (University of Chile), Éric Tanter (University of Chile)

**Dissecting Widening: Separating Termination from Information**

Graeme Gange, Jorge A. Navas (SRI International), Peter Schachte, Harald Sondergaard, Peter J. Stuckey (Monash University)

**A Type-Based HFL Model Checking Algorithm**

Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada (University of Tokyo)

**Reducing Static Analysis Alarms based on Non-impacting Control Dependencies**

Tukaram Muske, Rohith Talluri (Tata Consultancy Services Ltd), Alexander Serebrenik (Eindhoven University of Technology)

**Factorization and Normalization, Essentially**

Beniamino Accattoli (Inria & Ecole Polytechnique), Claudia Faggian (IRIF), Giulio Guerrieri (University of Bath)

**Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion**

Masayuki Mizuno, Eijiro Sumii (Tohoku University)

**Recursion Schemes in Coq**

Kosuke Murata (Kyushu Institute of Technology), Kento Emoto (University of Tokyo)

**Lightweight Functional Logic Meta-Programming**

Nada Amin (Harvard University), William E. Byrd (University of Alabama), USA, Tiark Rompf (Purdue University)

**Mimalloc: Free List Sharding in Action**

Daan Leijen, Ben Zorn, Leonardo De Moura (Microsoft Research)

**LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL**

Yutaka Nagashima (Czech Technical University and University of Innsbruck)

**Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps**

Taolue ChenBirkbeck (University of London), Jilong He (Chinese Academy of Sciences), Yu-Ping Wang (Tsinghua University), Zhilin Wu (Chinese Academy of Sciences), Jun Yan (Chinese Academy of Sciences)

**Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects**

Thomas Dickerson (Brown University), Paul Gazzillo (University of Central Florida), Maurice Herlihy (Brown University), Eric Koskinen (Stevens Institute of Technology)

**Transactional Forest: A DSL for Managing Concurrent Filestores**

Jonathan DiLorenzo (Cornell University), Kathryn Mancini (Cornell University), Kathleen Fisher (Tufts University), Nate Foster (Cornell University)

**J-ReCoVer: Java Reducer Commutativity Veriﬁer [Tool Paper]**

Yu-Fang Chen (Academia Sinica), Chang-Yi Chiang (National Taipei University), Lukas Holik (Brno University of Technology), Wei-Tsung Kao (Academia Sinica), Hsin-Hung Lin (Academia Sinica), Yean-Fu Wen (National Taipei University), Tomas Vojnar (Brno University of Technology), Wei-Cheng Wu (Academia Sinica)

**Uniform Random Process Model Revisited**

Makoto Tatsuta (National Institute of Informatics), Koji Nakazawa (Nagoya University), Daisuke Kimura (Toho University)

**Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions**

Raimil Cruz (University of Chile), Éric Tanter (University of Chile)

**Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning**

Long H. Pham (Singapore University of Technology and Design), Jun Sun (Singapore Management University), Quang Loc Le (Teesside University)

**Pumping, With or Without Choice**

Aquinas Hobor (National University of Singapore), Elaine Li (Runtime Verification, Inc.), Frank Stephan (National University of Singapore)

**Simulations in Rank-Based Buchi Automata Complementation**

Yu-Fang Chen (Academia Sinica), Vojtěch Havlena (Brno University of Technology), Ondrej Lengal (Brno University of Technology)

**Succinct Determinisation of Counting Automata via Sphere Construction**

Lukas Holik (Brno University of Technology), Tomas Vojnar (Brno University of Technology), Ondrej Lengal (Brno University of Technology), Lenka Turonova (Brno University of Technology), Margus Veanes (Microsoft Research), Olli Saarikivi