Programming Languages and Systems: 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2–6, 2018, Proceedings

Description

This book constitutes the proceedings of the 16th Asian Symposium on Programming Languages and Systems, APLAS 2018, held in Wellington, New Zealand, in December 2018. The 22 papers presented in this volume were carefully reviewed and selected from 51 submissions. They are organized in topical sections named: types; program analysis; tools; functional programs and probabilistic programs; verification; logic; and continuation and model checking. Front Matter ....Pages I-XI Front Matter ....Pages 1-1 Non-linear Pattern Matching with Backtracking for Non-free Data Types (Satoshi Egi, Yuichi Nishiwaki)....Pages 3-23 Factoring Derivation Spaces via Intersection Types (Pablo Barenbaum, Gonzalo Ciruelos)....Pages 24-44 Types of Fireballs (Beniamino Accattoli, Giulio Guerrieri)....Pages 45-66 Front Matter ....Pages 67-67 On the Soundness of Call Graph Construction in the Presence of Dynamic Language Features - A Benchmark and Tool Evaluation (Li Sui, Jens Dietrich, Michael Emery, Shawn Rasheed, Amjed Tahir)....Pages 69-88 Complexity Analysis of Tree Share Structure (Xuan-Bach Le, Aquinas Hobor, Anthony W. Lin)....Pages 89-108 Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Models (Thibault Suzanne, Antoine Miné)....Pages 109-128 Front Matter ....Pages 129-129 Scallina: Translating Verified Programs from Coq to Scala (Youssef El Bakouny, Dani Mezher)....Pages 131-145 HoIce: An ICE-Based Non-linear Horn Clause Solver (Adrien Champion, Naoki Kobayashi, Ryosuke Sato)....Pages 146-156 Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof General (Hideyuki Kawabata, Yuta Tanaka, Mai Kimura, Tetsuo Hironaka)....Pages 157-165 The Practice of a Compositional Functional Programming Language (Timothy Jones, Michael Homer)....Pages 166-177 Front Matter ....Pages 179-179 New Approaches for Almost-Sure Termination of Probabilistic Programs (Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee)....Pages 181-201 Particle-Style Geometry of Interaction as a Module System (Ulrich Schöpp)....Pages 202-222 Automated Synthesis of Functional Programs with Auxiliary Functions (Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada)....Pages 223-241 Front Matter ....Pages 243-243 Modular Verification of SPARCv8 Code (Junpeng Zha, Xinyu Feng, Lei Qiao)....Pages 245-263 Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine (Fabian Kunze, Gert Smolka, Yannick Forster)....Pages 264-283 Automated Modular Verification for Relaxed Communication Protocols (Andreea Costea, Wei-Ngan Chin, Shengchao Qin, Florin Craciun)....Pages 284-305 Front Matter ....Pages 307-307 Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks (Taro Sekiyama, Kohei Suenaga)....Pages 309-328 On the Complexity of Pointer Arithmetic in Separation Logic (James Brotherston, Max Kanovich)....Pages 329-349 A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints (Quang Loc Le, Mengda He)....Pages 350-372 Front Matter ....Pages 373-373 Certifying CPS Transformation of Let-Polymorphic Calculus Using PHOAS (Urara Yamada, Kenichi Asai)....Pages 375-393 Model Checking Differentially Private Properties (Depeng Liu, Bow-Yaw Wang, Lijun Zhang)....Pages 394-414 Shallow Effect Handlers (Daniel Hillerström, Sam Lindley)....Pages 415-435 Back Matter ....Pages 437-437