Programming Languages and Systems: 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1–4, 2019, Proceedings

Description

This book constitutes the proceedings of the 17th Asian Symposium on Programming Languages and Systems, APLAS 2019, held in Nusa Dua, Bali, Indonesia, in December 2019. The 22 papers presented in this volume were carefully reviewed and selected from 50 submissions. They were organized in topical sections named: Invited Papers, Types, Program Analysis, Semantics, Language Design and Implementation, Concurrency, Verification, and Logic and Automata. Front Matter ....Pages i-xiii Front Matter ....Pages 1-1 Proving that Programs Are Differentially Private (Annabelle McIver, Carroll Morgan)....Pages 3-18 On Strings in Software Model Checking (Hossein Hojjat, Philipp Rümmer, Ali Shamakhi)....Pages 19-30 Front Matter ....Pages 31-31 Manifest Contracts with Intersection Types (Yuki Nishida, Atsushi Igarashi)....Pages 33-52 A Dependently Typed Multi-stage Calculus (Akira Kawata, Atsushi Igarashi)....Pages 53-72 Existential Types for Relaxed Noninterference (Raimil Cruz, Éric Tanter)....Pages 73-92 Front Matter ....Pages 93-93 Dissecting Widening: Separating Termination from Information (Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey)....Pages 95-114 Reducing Static Analysis Alarms Based on Non-impacting Control Dependencies (Tukaram Muske, Rohith Talluri, Alexander Serebrenik)....Pages 115-135 A Type-Based HFL Model Checking Algorithm (Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada)....Pages 136-155 Front Matter ....Pages 157-157 Factorization and Normalization, Essentially (Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri)....Pages 159-180 Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion (Masayuki Mizuno, Eijiro Sumii)....Pages 181-201 Recursion Schemes in Coq (Kosuke Murata, Kento Emoto)....Pages 202-221 Front Matter ....Pages 223-223 Lightweight Functional Logic Meta-Programming (Nada Amin, William E. Byrd, Tiark Rompf)....Pages 225-243 Mimalloc: Free List Sharding in Action (Daan Leijen, Benjamin Zorn, Leonardo de Moura)....Pages 244-265 LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL (Yutaka Nagashima)....Pages 266-287 Front Matter ....Pages 289-289 Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps (Jinlong He, Taolue Chen, Ping Wang, Zhilin Wu, Jun Yan)....Pages 291-312 Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects (Thomas Dickerson, Eric Koskinen, Paul Gazzillo, Maurice Herlihy)....Pages 313-331 TxForest: A DSL for Concurrent Filestores (Jonathan DiLorenzo, Katie Mancini, Kathleen Fisher, Nate Foster)....Pages 332-354 Front Matter ....Pages 355-355 J-ReCoVer: Java Reducer Commutativity Verifier (Yu-Fang Chen, Chang-Yi Chiang, Lukáš Holík, Wei-Tsung Kao, Hsin-Hung Lin, Tomáš Vojnar et al.)....Pages 357-366 Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions (Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura)....Pages 367-387 Uniform Random Process Model Revisited (Wenbo Zhang, Huan Long, Xian Xu)....Pages 388-404 Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning (Long H. Pham, Jun Sun, Quang Loc Le)....Pages 405-424 Front Matter ....Pages 425-425 Pumping, with or Without Choice (Aquinas Hobor, Elaine Li, Frank Stephan)....Pages 427-446 Simulations in Rank-Based Büchi Automata Complementation (Yu-Fang Chen, Vojtěch Havlena, Ondřej Lengál)....Pages 447-467 Succinct Determinisation of Counting Automata via Sphere Construction (Lukáš Holík, Ondřej Lengál, Olli Saarikivi, Lenka Turoňová, Margus Veanes, Tomáš Vojnar)....Pages 468-489 Back Matter ....Pages 491-492