Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings (Lecture Notes in Computer Science)

This book constitutes the proceedings of the 20th Asian Symposium on Programming Languages and Systems, APLAS 2022, held in Auckland, New Zealand, in December 2022. The 10 papers presented in this volume were carefully reviewed and selected from 22 submissions. They were organized in topical sections as follows: Semantics and Analysis; Testing and Verification; Types. Preface Organization Verification of Concurrent Programs Under Release Acquire (Invited Talk) Contents Semantics and Analysis An Algebraic Theory for Shared-State Concurrency 1 Introduction 2 Overview 2.1 Global-State (for Sequential Computation) 2.2 Shared-State 2.3 Denotations 2.4 Program Transformations 2.5 Caveats and Limitations 3 Equational Theory 4 A Monad for Shared-State 4.1 Difficulty of Term Normalization 4.2 Traces 4.3 Model Definition 4.4 Correspondence to Non-deterministic Global-State 4.5 Representation Theorem 4.6 Synchronization 5 Denotational Semantics 6 Metatheoretical Results 6.1 Example Transformations 7 Conclusion, Related Work, and Future Work References Decoupling the Ascending and Descending Phases in Abstract Interpretation 1 Introduction 2 Background 3 Decoupling the Ascending and Descending Phases 4 Experimental Evaluation 4.1 A Detailed Example 5 Related Work 6 Conclusion References Inferring Region Types via an Abstract Notion of Environment Transformation 1 Introduction 2 Background 2.1 Featherweight Java 2.2 Access Graphs 3 A Theory of Abstract Transformations 3.1 Types and Environments 3.2 Abstract Transformations 3.3 Operations on Abstract Transformations 4 Type Inference via Abstract Transformations 4.1 Region Type System 4.2 Inferring Region Types via Abstract Transformations 5 Conclusion, Implementation and Discussion References Testing and Verification RHLE: Modular Deductive Verification of Relational Properties 1 Introduction 2 The FunIMP Language 3 Approximating FunIMP Behaviors 3.1 Universal Executions 3.2 Existential Executions 3.3 Approximating Behaviors 4 RHLE 4.1 Synchronous Rules 4.2 Soundness 5 Verification 6 Implementation and Evaluation 7 Related Work 8 Conclusion References Automated Temporal Verification for Algebraic Effects 1 Introduction 2 Overview 2.1 A Sense of ContEffs in File I/O 2.2 Effects Inferences via a Fixpoint Calculation 2.3 The TRS: To Prove Effects Inclusions 3 Language and Specifications 3.1 The Target Language 3.2 The Specification Language 3.3 Instrumented Semantics 4 Forward Verification 4.1 Forward Verification Rules 4.2 Fixpoint Computation 4.3 Reasoning in the Handling Program 5 Temporal Verification via a TRS 5.1 Rewriting Rules 6 Implementation and Evaluation 6.1 Case Studies 7 Related Work 8 Conclusion References Model-Based Fault Classification for Automotive Software 1 Introduction 2 Formal Model 3 Fault Localization 4 Fault Explanation 5 Fault Classification 6 Hoare Proofs with Timing 7 Application in Automotive Software 8 Related Work References Types Characterizing Functions Mappable over GADTs 1 Introduction 2 The Problem and Its Solution: An Overview 3 The Algorithm 4 Examples 5 Conclusion, Related Work, and Future Directions References Applicative Intersection Types 1 Introduction 2 Overview 2.1 Background 2.2 Applications of the Merge Operator 2.3 Challenges in the Design of the Semantics 2.4 Key Ideas and Results 3 Applicative Subtyping 3.1 Types and Subtyping 3.2 Applicative Subtyping 3.3 Metatheory 4 A Calculus with an Unrestricted Merge Operator 4.1 Syntax 4.2 Typing 4.3 Semantics 4.4 Type Soundness 5 A Calculus with a Disjoint Merge Operator 5.1 Disjointness 5.2 Typing and Semantics 5.3 Type Soundness and Determinism 6 Related Work 7 Conclusion and Future Work References A Calculus with Recursive Types, Record Concatenation and Subtyping 1 Introduction 2 Overview 2.1 Background: Disjoint Intersection Types 2.2 i: Adding Recursive Types to i 2.3 Disjointness for Recursive Types 3 Static Semantics of i 3.1 Syntax and Subtyping 3.2 Decidability 3.3 Disjointness 3.4 Completeness of Disjointness 3.5 Bidirectional Typing 4 Dynamic Semantics of i 4.1 A Type-Directed Operational Semantics for i 4.2 Reduction 4.3 Determinism 4.4 Type Safety 5 Discussion and Related Work 6 Conclusion References Novice Type Error Diagnosis with Natural Language Models 1 Introduction 2 Approach 2.1 Language Models 2.2 The Pre-training and Fine-Tuning Scheme 2.3 Type Error Diagnosis as Token Classification 2.4 Structural Probe 3 Dataset and Evaluation Metric 3.1 Pre-training Dataset 3.2 Fine-Tuning Dataset 3.3 Evaluation Metric 4 Evaluation 4.1 Performance of Different Models (RQ1) 4.2 Effectiveness of Model Sizes and Transfer Learning (RQ2) 4.3 Generalization Ability of Language Models (RQ3) 4.4 Explaining Performance Difference by the Structural Probe (RQ4) 5 Related Work 6 Conclusions and Future Work References Author Index