Programming Languages and Systems. 31st European Symposium on Programming, ESOP 2022 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022 Munich, Germany, April 2–7, 2022. Proceedings

ETAPS Foreword
Preface
Organization
Contents
Categorical Foundations of Gradient-Based Learning
	1 Introduction
	2 Categorical Toolkit
		2.1 Parametric Maps
		2.2 Lenses
		2.3 Parametric Lenses
		2.4 Cartesian Reverse Differential Categories
	3 Components of learning as Parametric Lenses
		3.1 Models as Parametric Lenses
		3.1 Models as Parametric Lenses
		3.2 Loss Maps as Parametric Lenses
		3.3 Learning Rates as Parametric Lenses
		3.4 Optimisers as Reparameterisations
	4 Learning with Parametric Lenses
		4.1 Supervised Learning of Parameters
		4.2 Deep Dreaming: Supervised Learning of Inputs
	5 Implementation
		5.1 Constructing a Model with Lens and Para
		5.2 Learning
	6 Related Work
	7 Conclusions and Future Directions
	References
Compiling Universal Probabilistic Programming Languages with Efficient Parallel Sequential Monte Carlo Inference
	1 Introduction
	2 Miking CorePPL
		2.1 Design Considerations
		2.2 Syntax and Semantics
	3 PPL control-flow graphs and RootPPL
		3.1 PPL Control-Flow Graphs
		3.2 SMC and PCFGs
		3.3 RootPPL
	4 Compiling to PCFGs
		4.1 Function Decomposition Example
		4.2 Function Decomposition Algorithm
		4.3 CorePPL-to-RootPPL Compiler
		4.4 Compiler Strengths and Limitations
	5 Evaluation
		5.1 Experiment: Constant-Rate Birth Death
		5.2 Experiment: Vector-Borne Disease
		5.3 Experiment: CRBD with Variance-Reducing Techniques
	6 Related Work
	7 Conclusion
	References
Foundations for Entailment Checking in Quantitative Separation Logic
	1 Introduction
	2 (Quantitative) Separation Logic
		2.1 Program States
		2.2 Separation Logic
		2.3 Quantitative Separation Logic
	3 Entailments in Probabilistic Program Verification
		3.1 Heap-manipulating pGCL
		3.2 Weakest Liberal Preexpectations
		3.3 Interfered Swap
		3.4 Avoiding Magic Wands
		3.5 Randomized List Population
	4 Quantitative Entailment Checking
		4.1 Idea and Key Observations
		4.2 Constructing Finite Overapproximations of Eval (f)
		4.3 Lower Bounding QSL [A] by SL [A] Formulae
	5 Complexity
	6 Application: Decidable hpGCL Verification
		6.1 Quantitative Symbolic Heaps
	7 Related Work
	8 Discussion and Conclusion
	References
Extracting total Amb programs from proofs
	1 Introduction
	2 Denotational semantics of globally angelic choice
		2.1 Programs and types
		2.2 Denotational semantics
	3 Operational semantics
		3.1 Reduction to weak head normal form
		3.2 Making choices
		3.3 Computational adequacy: Matching denotational and operational semantics
	4 CFP (Concurrent Fixed Point Logic)
		4.1 Syntax
		4.2 Proof rules
		4.3 Tarskian semantics, axioms and classical logic
	5 Program extraction
		5.1 Realizability
		5.2 Partial correctness and concurrency
		5.3 Soundness and program extraction
	6 Application
	7 Implementation
	8 Conclusion
		8.1 Related work
		8.2 Modelling locally angelic choice
		8.3 Markov\'s principle with restriction
		8.4 Further directions for research
	References
Why3-do: The Way of Harmonious Distributed System Proofs
	1 Introduction
	2 The Why3 Languages in a Nutshell
	3 Distributed Systems and Models
	4 The Basic Message-Passing Model
	5 Trace Specifications
	6 Locally Shared Memory Model
	7 Related Work
	8 Conclusion
	References
Relaxed virtual memory in Armv8-A
	1 Introduction
	2 Background: A Crash Course on Virtual Memory
		2.1 Virtualising addressing
		2.2 The translation-table walk
		2.3 Multiple stages of translation
		2.4 Caching translations in TLBs
	3 Concurrency Architecture Design Questions
		3.1 Coherence with respect to physical or virtual addresses
		3.2 Relaxed behaviour from TLB caching
		3.3 Relaxed behaviour of translation-walk non-TLB reads
		3.4 Further issues
	4 Virtual memory in the pKVM production hypervisor
	5 Model
	6 Tooling
		6.1 Isla-based model evaluation
		6.2 Experimental testing of hardware
	7 Related work
	8 Acknowledgments
	References
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture
	1 Introduction
	2 Overview of the Morello CHERI Architecture
		2.1 CHERI Capabilities on Morello
		2.2 Capabilities in Registers and Memory
		2.3 Capability-aware Instructions
		2.4 Domain Transition
		2.5 Exceptions and the Memory Management Unit
		2.6 Using CHERI in Software
	3 Concrete Semantics of Morello
	4 Abstract Formal Model of Capability Monotonicity
		4.1 ISA Abstraction
		4.2 CHERI ISA Parameters
		4.3 Capability Abstraction
		4.4 CHERI ISA Intra-instruction Properties
		4.5 Capability Monotonicity Theorem
	5 Proof of Capability Monotonicity in Morello
		5.1 Instantiation of the Abstract Model
		5.2 Manual Proofs about Capability Encoding Functions
		5.3 Proof Engineering
		5.4 Bugs and Issues Found
	6 Validating the Concrete Semantics
	7 Model-based Test Generation
	8 Related Work
	References
The Trusted Computing Base of the CompCert Verified Compiler
	1 Introduction
	2 The Coq Proof Assistant
		2.1 Issues in Coq Proof Checking
		2.2 Issues in Coq Extraction
	3 Use of Axioms in Coq
		3.1 Logical Inconsistency
		3.2 Mismatches between Coq and OCaml
		3.3 Interfacing External Code as Pure Functions
		3.4 Pointer Equality and Hash-Consing
	4 Front-end and semantic issues
	5 Assembly back-end issues
		5.1 Printing Issues
		5.2 Pseudo-Instructions
		5.3 Microarchitectural Concerns
		5.4 Assembling and Linking
	6 Modeling and Application Binary Interface Issues
		6.1 Modeling of Values
		6.2 Foreign Function Interface
		6.3 Runtime System
	7 Insights and Conclusion
	References
View-Based Owicki–Gries Reasoning for Persistent x86-TSO
	1 Introduction
	2 Overview and Motivation
		2.1 Px86view at a Glance
		2.2 PIEROGI: View-Based Owicki–Gries Reasoning for Px86view
	3 The PIEROGI Proof rules and Reasoning Principles
		3.1 The PIEROGI Programming Language
		3.2 View-Based Expressions
		3.3 Owicki–Gries Reasoning
		3.4 PIEROGI Proof rules
	4 Examples
	5 PIEROGI Soundness
		5.1 The Px86view Model
		5.2 The Semantics of PIEROGI Assertions
		5.3 Soundness of PIEROGI
	6 Mechanisation
	7 Related Work
	References
Abstraction for Crash-Resilient Objects
	1 Introduction
	2 Key Challenges and Ideas
		2.1 Library Specifications
		2.2 Client-Library Interaction Using Explicit Persist Instructions
		2.3 Handling Calling Policies
	3 NVM Programs: Syntax and Semantics
		3.1 Program Syntax
		3.2 Program Semantics
	4 The PSC Memory System
		4.1 Linking Programs and Memories
		4.2 Extending PSC for Library Abstraction
		4.3 Separation Properties
	5 Libraries and Their Clients
	6 The Library Abstraction Theorem
	7 An Application: Persistent Pairs
	8 Related and Future Work
	References
Static Race Detection for Periodic Programs
	1 Introduction
	2 Overview
	3 Periodic Programs
	4 Data Races
	5 Response Time and its Computation
		5.1 Computing Response time without Locks
	6 Rules for Disjointness
		6.1 Disjoint Block Rules
		6.2 Computing the value m in Rule 5
		6.3 Race Detection Algorithm
	7 Experimental Evaluation
		7.1 Implementation
		7.2 Benchmarks
		7.3 Results
	8 Related Work
	9 Conclusion
	References
Probabilistic Total Store Ordering
	1 Introduction
	2 Preliminaries
	3 Concurrent Programs
	4 Operational Semantics
		4.1 Configurations
		4.2 The Classical TSO Semantics
		4.3 Adding Probabilities: PTSO
	5 PTSO: Concepts and Properties
		5.1 Left-Orientedness and Attractors
	6 Qualitative (Repeated) Reachability
		6.1 Almost-Sure Reachability
		6.2 Almost-Sure Repeated Reachability
		6.3 Almost-Never (Repeated) Reachability
		6.4 Decidability and Complexity
	7 Quantitative (Repeated) Reachability
		7.1 Approximate Quantitative Reachability
		7.2 Approximate Quantitative Repeated Reachability
	8 Expected Average Costs
		8.1 Computing costs over runs
		8.2 Eagerness
		8.3 The Algorithm
	9 Conclusions, Discussions, and Perspectives
	References
Linearity and Uniqueness: An Entente Cordiale
	1 Introduction
	2 Key Ideas
		2.1 Are linearity and uniqueness (essentially) the same?
		2.2 Are linearity and uniqueness dual?
	3 The Linear-Cartesian-Unique Calculus
		3.1 Typing
		3.2 Equational theory
		3.3 Exploiting uniqueness for mutation
		3.4 Operational heap model
		3.5 Metatheory
	4 Implementation
		4.1 Frontend
		4.2 Compilation and Evaluation
	5 Related Work
	6 Future Work
	7 Conclusion
	References
A Framework for Substructural Type Systems
	1 Introduction
	2 Vectors over semirings
	3 Bunched Typing Rules
	4 Generic syntax
		4.1 Descriptions of Systems
		4.2 Terms of a System
		4.3 Other syntaxes and syntactic forms
	5 Environments
	6 Semantics
		6.1 A layer of syntax is functorial
		6.2 The Kripke function space
		6.3 Semantic traversal
	7 Example traversals
		7.1 Renaming and substitution
		7.2 A usage elaborator
		7.3 A denotational semantics
	8 Conclusions
	References
A Dependent Dependency Calculus
	1 Dependency Analysis
	2 Irrelevance and Dependent Types
		2.1 Run-time irrelevance
		2.2 Compile-time Irrelevance
		2.3 Strong Irrelevant Σ-types
	3 A Simple Dependency Analyzing Calculus
		3.1 Type System
		3.2 Meta-theoretic Properties
		3.3 A Syntactic Proof of Non-interference
		3.4 Relation with Sealing Calculus and Dependency Core Calculus
	4 A Dependent Dependency Analyzing Calculus
		4.1 DDC^T : Π-types
		4.2 DDC^T : Σ-types
		4.3 Embedding SDC into DDC^T
		4.4 Run-time Irrelevance
	5 DDC: Run-time and Compile-time Irrelevance
		5.1 Towards Compile-time Irrelevance
		5.2 DDC: Basics
		5.3 Π-types
		5.4 Σ-types
		5.5 Non-interference
		5.6 Consistency of Equality
		5.7 Soundness theorem
	6 Type Checking
	7 Discussions and Related Work
		7.1 Irrelevance in Dependent Type Theories
		7.2 Quantitative Type Systems
		7.3 Dependency Analysis and Dependent Type Theory
	8 Conclusion
	9 Acknowledgments
	References
Polarized Subtyping
	1 Introduction
	2 Equirecursive Call-by-Push-Value
		2.1 Dynamics
		2.2 Some Sample Programs
	3 Semantic Typing
		3.1 Semantic Typing with Observation Depth
		3.2 Properties of Semantic Typing
	4 Subtyping
		4.1 Empty and Full Types
		4.2 Syntactic Subtyping
	5 Syntactic Typing and Soundness
	6 Bidirectional Typing
	7 Interpretation of Isorecursive Types
	8 Call-by-Name and Call-by-Value
		8.1 Call-by-name
		8.2 Call-by-Value
	9 Related Work and Discussion
	10 Conclusion
	References
Structured Handling of Scoped Effects
	1 Introduction
	2 Scoped Effects for the Working Programmer
		2.1 Handlers of Algebraic Effects
		2.2 Scoped Operations as Handlers Are Not Modular
		2.3 Scoped Effects and Functorial Algebras
	3 Categorical Foundations for Scoped Operations
		3.1 Syntax and Semantics of Algebraic Operations
		3.2 Syntax of Scoped Operations
		3.3 Functorial Algebras of Scoped Operations
		3.4 Interpreting with Functorial Algebras
	4 Comparing the Models of Scoped Operations
		4.1 Interpreting Scoped Operations with Eilenberg-Moore Algebras
		4.2 Indexed Algebras of Scoped Effects
		4.3 Comparison of Resolutions
		4.4 Translating EM Algebras to Functorial Algebras
		4.5 Translating Functorial Algebras to Indexed Algebras
	5 Fusion Laws of Interpretation
		5.1 Fusion Laws of Interpretation
	6 Related Work
	7 Conclusion
	References
Region-based Resource Management and Lexical Exception Handlers in Continuation-Passing Style
	1 Introduction
	2 Overview
		2.1 Regions for Resources
		2.2 Regions for Exception Handlers
		2.3 Combining Resources and Exceptions
		2.4 First-Class Functions
	3 A Language with Regions, Resources, and Exceptions
		3.1 Syntax
		3.2 Typing
		3.3 Operational Semantics
		3.4 Resource Pools
		3.5 Exceptions
		3.6 Combining Resource Pools and Exceptions
		3.7 Metatheory of Λ_ρ
	4 Translation of Regions, Pools, and Exceptions to CPS
		4.1 Translation of Core Λ_ρ
		4.2 Resource Pools
		4.3 Exceptions
		4.4 Combining Resource Pools and Exceptions
		4.5 Simulation of the Machine Semantics by the CPS translation
	5 Related Work
	6 Conclusion
	References
A Predicate Transformer for Choreographies Computing Preconditions in Choreographic Programming
	1 Introduction
		1.1 Background: Choreographic Programming by Example
		1.2 Related Work: State of the Art & Open Problems
		1.3 Contributions of This Paper
		1.4 Key Challenge: How to Check If Unanimity Is Guaranteed?
		1.5 Organisation of This Paper
	2 Motivating Examples
	3 Setting the Stage: Data and Conditions
		3.1 Data
		3.2 Conditions
	4 Global Programs: Base Calculus
		4.1 Syntax and Semantics
		4.2 Predicate Transformer
		4.3 Deadlock Freedom and Functional Correctness
	5 Global Programs: If/While-Statements
		5.1 Syntax and Semantics
		5.2 Predicate Transformer
		5.3 Deadlock Freedom and Functional Correctness
	6 Global Programs: Non-Blocking If/While-Statements
		6.1 Syntax and Semantics
		6.2 Predicate Transformer
		6.3 Main Theorem: Deadlock Freedom and Functional Correctness
	7 Local Programs and Projection
		7.1 Syntax and Semantics
		7.2 Operational Equivalence
	8 Conclusion
	References
Comparing the expressiveness of the π-calculus and CCS
	1 Introduction
	2 CCS
	3 CCS_γ
	4 Strong barbed bisimilarity
	5 The π-calculus
	6 The semantics of the π-calculus
	7 Valid translations
	8 The unencodability of π into CCS
	9 A valid translation of π_IM into CCS_γ
	10 The ideas behind this encoding
	11 Triggering
	12 Examples
	13 The unencodability of CCS into π
	14 Related work
	15 Conclusion
	References
Concurrent NetKAT Modeling and analyzing stateful, concurrent networks
	1 Introduction
	2 Overview
	3 Concurrent NetKAT
		3.1 Pomsets and pomset languages
		3.2 CNetKAT: syntax and semantics
		3.3 Is CNetKAT conservative over NetKAT and POCKA?
		3.4 Axiomatization
	4 Soundness and Completeness
	5 Examples
		5.1 Running Example
		5.2 Stateful Load Balancer, Cache, and Firewall
	6 Related Work
	7 Discussion
	References
Author Index