Programming Languages and Systems (Lecture Notes in Computer Science)

✍ Scribed by Thomas Wies (editor)

• Publisher: Springer
• Year: 2023
• Tongue: English
• Leaves: 579
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

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