Programming Languages and Systems. 19th Asian Symposium, APLAS 2021 Chicago, IL, USA, October 17–18, 2021 Proceedings

Description

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