This open access book constitutes the proceedings of the 32nd European Symposium on Programming, ESOP 2023, which was held during April 22-27, 2023, in Paris, France, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023. The 20 regular papers presented in this volume were carefully reviewed and selected from 55 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems. ETAPS Foreword Preface Organization Contents Logics for Extensional, Locally Complete Analysis via Domain Refinements 1 Introduction 2 Background 2.1 Abstract Interpretation 2.2 Regular Commands. 3 Local Completeness Logic 4 Refining Abstract Domain 4.1 Logical Completeness 4.2 Derived Refinement Rules 4.3 Choosing The Refinement 5 Conclusions Appendix A Proofs and Supplementary Material A.1 Extensional Soundness (Theorem 2) A.2 Soundness and Completeness of (refine-ext ) A.3 Derived Refinement Rules References Clustered Relational Thread-ModularAbstract Interpretation with Local Traces 1 Introduction 2 Relational Domains 3 A Local Trace Semantics 4 Relational Analyses as Abstractions of Local Traces 5 Refinement via Finite Abstractions of Local Traces 6 Analysis of Thread Ids and Uniqueness 7 Exploiting Thread IDs to Improve Relational Analyses 8 Exploiting Clustered Relational Domains 9 Experimental Evaluation 10 Related Work 11 Conclusion and Future Work References Adversarial Reachability for Program-level Security Analysis 1 Introduction 2 Motivation 2.1 Fault Injection across Security Fields 2.2 Motivating Example 3 Background 3.1 Software-implemented Fault Injection (SWiFI) 3.2 Standard Reachability Formalization 3.3 Symbolic Execution 4 Adversarial Reachability 5 Forkless Adversarial Symbolic Execution (FASE) 5.1 Modelling Faults via Forkless Encoding 5.2 Building Adversarial Path Predicates 5.3 Algorithm Properties 5.4 Optimization via Early Detection of Fault Saturation (FASE-EDS) 5.5 Optimization via Injection on Demand (FASE-IOD) 5.6 Optimizations Combination 6 Implementation 7 Evaluation 7.1 Experimental Setting 7.2 Correctness and Completeness in Practice (RQ1) 7.3 Scalability (RQ2) 7.4 Performance Optimization (RQ3) 7.5 Other Experiments and Fault Models 8 Case Study: the WooKey Bootloader 9 Discussion 10 Related Work 11 Conclusion Automated Grading of Regular Expressions Builtin Types Viewed as Inductive Families Pragmatic Gradual Polymorphism with References Modal Crash Types for Intermittent Computing Gradual Tensor Shape Checking A Type System for Effect Handlersand Dynamic Labels Interpreting Knowledge-based Programs Contextual Modal Type Theory with Polymorphic Contexts A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests 1 Introduction 2 Overview 3 Introducing Skip-free GKAT 3.1 Skip-free Semantics 3.2 Axioms 4 1-free Star Expressions 5 Completeness for Skip-free Bisimulation GKAT 5.1 Transforming skip-free automata to labelled transition systems 5.2 Translating Syntax 6 Completeness for Skip-free GKAT 7 Relation to GKAT 7.1 Bisimulation semantics 7.2 Language semantics 7.3 Equivalences 8 Related Work 9 Discussion References Quorum Tree Abstractions of Consensus Protocols MAG: Types for Failure-Prone Communication System F-mu-omega with Context-free Session Types Safe Session-Based Concurrency with Shared Linear State Bunched Fuzz: Sensitivity for Vector Metrics Fast and Correct Gradient-Based Optimisationfor Probabilistic Programming via Smoothing Type-safe Quantum Programming in Idris Automatic Alignment in Higher-Order Probabilistic Programming Languages 1 Introduction 2 A Motivating Example 2.1 Aligned SMC 2.2 Aligned Lightweight MCMC 3 Syntax and Semantics 3.1 Syntax 3.2 Semantics 4 Alignment Analysis 4.1 A-Normal Form and Alignment 4.2 Alignment Analysis 4.3 Dynamic Alignment 5 Aligned SMC and MCMC 5.1 Aligned SMC 5.2 Aligned Lightweight MCMC 6 Implementation 7 Evaluation 7.1 SMC: Constant Rate Birth-Death (CRBD) 7.2 SMC: Cladogenetic Diversification Rate Shift (ClaDS) 7.3 SMC: State-Space Aircraft Localization 7.4 MCMC: Latent Dirichlet Allocation (LDA) 7.5 MCMC: Constant Rate Birth-Death (CRBD) 8 Related Work 9 Conclusion References Correction to: Programming Languages and Systems Correction to: T. Wies (Ed.): Programming Languages and Systems, LNCS 13990, https://doi.org/10.1007/978-3-031-30044-8 Author Index
