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

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