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 Verifier [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