Programming Languages and Systems: 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17–18, 2021, Proceedings (Lecture Notes in Computer Science Book 13008)

This book constitutes the proceedings of the 19th Asian Symposium on Programming Languages and Systems, APLAS 2021, held in Chicago, USA, in October 2021.\* The 17 papers presented in this volume were carefully reviewed and selected from 43 submissions. They were organized in topical sections named: analysis and synthesis, compilation and transformation, language, and verification. \* The conference was held in a hybrid format due to the COVID-19 pandemic. Preface Organization Abstracts of Invited Talks Solidifying and Advancing the Software Foundations A Separation Logic for Probabilistic Independence Contents Analysis and Synthesis Scalable and Modular Robustness Analysis of Deep Neural Networks 1 Introduction 2 Overview 2.1 Preliminary Description on Abstract Domain 2.2 Abstract Interpretation on the Example Network 2.3 Scaling up with Block Summarization 3 Network Block Summarization 3.1 Network Analysis with Modularization 3.2 Summarization Within Block 3.3 Summarization Defined over Input Layer 4 Experiment 4.1 Experiment Setup 4.2 Experiments on Fully-Connected and Convolutional Networks 4.3 Experiments on Residual Networks 5 Discussion 6 Related Work 7 Conclusion References Function Pointer Eliminator for C Programs 1 Introduction 2 The Function Pointer Eliminator FPE 2.1 Usage of FPE 2.2 Implementation of FPE 2.3 Analyzer Module (A-module) 2.4 Transformer Module (T-module) 3 Discussion 4 Experimental Results 5 Conclusion A Screenshot B Examples B.1 Example B.2 Example B.3 Example B.4 Example B.5 Example B.6 Example B.7 Example References PyCT: A Python Concolic Tester 1 Introduction 2 Object-Oriented Concolic Testing Algorithm 3 Function Support and Implementation 4 Constant Upcasting 5 Experiment Results References Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications 1 Introduction 2 Motivating Example 3 Preliminaries 4 The SynthSynthesizer 5 Evaluation 5.1 Interface Implementations 5.2 User Study 6 Related Work 7 Conclusions A Appendix A.1 TSL and its Decidability A.2 Experimental Results A.3 User Study Questions A.4 User Study Results Visualizations References Server-Side Computation of Package Dependencies in Package-Management Systems 1 Introduction 2 Package Managers 2.1 Package Managers for Programming Languages and Operating Systems 2.2 Package Dependencies 3 Algorithms 3.1 Initializing Package-Dependency Graph 3.2 Computing the Set of Indirectly-Dependent Packages for Every Package 3.3 Adding Packages to the Server 4 Parallelization 4.1 Initializing Package-Dependency Graph 4.2 Computing the Set of Indirectly-Dependent Packages for Every Package in Parallel 4.3 Adding Packages to the Server 5 Implementation 6 Experiments 6.1 Comparison Between fpms and yarn 6.2 Initialization 6.3 Adding Packages 7 Discussions 7.1 Applicability to Other Package Managers 7.2 Complex Specification of Dependencies and Local Environments 7.3 Multiple Package Registries 7.4 Nix Package Manager 7.5 Dependencies in Build Systems 7.6 Security 8 Conclusions and Future Work References Compilation and Transformation Fully Abstract and Robust Compilation 1 Introduction 2 Fully Abstract and Robust Compilation 2.1 Fully Abstract Compilation 2.2 Robust Compilation 3 Comparing blackFAC and blackRHP 4 Secure Compilation, Categorically 4.1 Distributive Laws and Operational Semantics 4.2 Maps of Distributive Laws as Fully Abstract Compilers 5 Reconciling Fully Abstract and Robust Compilation 6 Related Work 7 Conclusions and Future Work References A Dictionary-Passing Translation of Featherweight Go 1 Introduction 2 Overview 2.1 FG by Example 2.2 Dictionary-Passing Translation 3 Featherweight Go 4 Target Language 5 Dictionary-Passing Translation 5.1 Translating Programs, Methods and Expressions 5.2 Translating Structural Subtyping and Type Assertions 6 Properties 7 Related Work and Conclusion References Hybrid Quantum-Classical Circuit Simplification with the ZX-Calculus 1 Introduction 2 Hybrid Quantum-Classical Circuits and the Grounded ZX-Calculus 3 Graph-Like Diagrams and Focused gFlow 4 Translation of Hybrid Quantum-Classical Circuits 5 Grounded ZX Optimization 5.1 Basic Simplification Rules 5.2 Ground-Cut Simplification 5.3 The Algorithm 6 Circuit Extraction 7 Circuit Classicalization 7.1 Local-Search Algorithm 8 Implementation 9 Discussion and Future Work References A Compilation Method for Dynamic Typing in ML 1 Introduction 1.1 Analysis of Dynamic Typing 1.2 Our Strategy and Contribution 1.3 Related Works 2 The Source Calculus 3 The Target Calculus and Compilation 3.1 The Target Calculus and Type Soundness 3.2 Type-Directed Compilation 4 Pattern Matching 5 Introduction of Existential Type Variables 5.1 The Source Calculus with Pattern Matching and Existential Types 6 Implementation and Applications 6.1 Pretty Printing/Serialization and Deserialization 6.2 Database Programming 6.3 Meta-programming 7 Conclusions References Language Design The Choice Construct in the Soufflé Language 1 Introduction 2 Motivating Example 3 Semantics of Choice 4 Implementation in Soufflé 5 Experiments 5.1 Rooted Spanning Tree 5.2 Other Applications 6 Related Work 7 Conclusion References Latent Effects for Reusable Language Components 1 Introduction 2 Background and Motivation 2.1 Modular Syntax and Semantics with Data Types à la Carte 2.2 Advanced, Non-modular Control-Flow Effects 2.3 Our Approach: Latent Effects 3 Latent Effects 3.1 Non-modular Definition of Lambda Abstraction 3.2 Modular Latent Effect Signatures and Trees, Naively 3.3 Trees with Support for Modular Handlers 3.4 Example: Two Modular Handlers for Function Abstractions 4 Case Studies 4.1 Call-by-Need Evaluation 4.2 Staging 4.3 Library Summary 5 Related Work 6 Conclusion References Adaptable Traces for Program Explanations 1 Introduction 2 Call-By-Named-Value Semantics 3 From Proof Trees to Traces 4 Trace Views as Explanations 4.1 Hiding Judgments and Subtraces 4.2 Applying Judgments and Factoring Traces 5 Trace Query Language 6 Related Work 7 Conclusions and Future Work References A Typed Programmatic Interface to Contracts on the Blockchain 1 Introduction 2 Motivation 3 Execution Model 3.1 Local Node 3.2 Global Structures 4 Operational Semantics 4.1 Cast Reductions 4.2 Smart Contracts 4.3 Queries 5 Properties 5.1 Properties of Blockchain State Transitions 5.2 Typing Related Properties 6 Related Work 7 Conclusion References Verification Simplifying Alternating Automata for Emptiness Testing 1 Introduction 2 Preliminaries 3 Basic Simplification 4 Local Determinisation (State Up-Shifting) 4.1 Up-Shifting of States 4.2 Preventing Nested Substitution 4.3 Purification 4.4 Local Determinisation Algorithm 5 Down-Shifting of States Towards Minimal Cut 6 Experimental Evaluation 6.1 Experiment ``Best of Checkers'' 6.2 Experiment ``Individual Checkers'' 6.3 Parametric LTL Benchmarks 6.4 Basic Simplification 6.5 Impact of Preprocessing on Size of Automata References Termination Analysis for the -Calculus by Reduction to Sequential Program Termination 1 Introduction 2 Source and Target Languages 2.1 -Calculus 2.2 Sequential Language 3 Basic Transformation 4 Improving Transformation Using Refinement Types 4.1 Refinement Type System 4.2 Program Transformation 4.3 Type Inference 5 Implementation and Preliminary Experiments 5.1 Implementation 5.2 Preliminary Experiments 6 Related Work 7 Conclusion References Proving LTL Properties of Bitvector Programs and Decompiled Binaries 1 Introduction 2 Motivating Examples 3 Preliminaries 4 Bitwise-Branching 5 Reachability of Bitvector Programs 6 Termination and LTL of Bitvector Programs 7 Case Study: LTL of Decompiled Binaries 7.1 Bitvector Operations in Lifted Binaries 7.2 DarkSea: A Toolchain for Temporal Verification of Lifted Binaries 7.3 Experiments 8 Related Work 9 Conclusion A Proof of Theorem1 References Solving Not-Substring Constraint with Flat Abstraction 1 Introduction 2 Preliminaries 3 String Constraints 4 Solving String Constraints with Flattening 4.1 (Parametric) Flat Languages 4.2 Flattening of String Constraints 4.3 String Constraint Solving Algorithm 5 Flattening of Not-Contains Constraints 5.1 Simplifying Assumptions 5.2 Construction of the Flattening Formula 6 Implementation and Evaluation 7 Conclusion and Future Work References Author Index