Programming Languages and Systems: 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and ... Computer Science and General Issues)

This open access book constitutes the proceedings of the 29th European Symposium on Programming, ESOP 2020, which was planned to take place in Dublin, Ireland, in April 2020, as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020. The actual ETAPS 2020 meeting was postponed due to the Corona pandemic. The papers deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems. ETAPS Foreword Preface Organization Formal Methods for Evolving Database Applications (Abstract of Keynote Talk) Contents Trace-Relating Compiler Correctness and Secure Compilation -0.8em Introduction Trace-Relating Compiler Correctness Property Mappings Trace Relations and Property Mappings Preservation of Subset-Closed Hyperproperties Instances of Trace-Relating Compiler Correctness Undefined Behavior Resource Exhaustion Different Source and Target Values Abstraction Mismatches Trace-Relating Compilation and Noninterference Preservation Trace-Relating Secure Compilation Trace-Relating Secure Compilation: A Spectrum of Trinities Instance of Trace-Relating Robust Preservation of Trace Properties Instances of Trace-Relating Robust Preservation of Safety and Hypersafety Related Work Conclusion and Future Work 2 Runners in action 1 Introduction 2 Algebraic effects, handlers, and runners 2.1 Algebraic effects and handlers 2.2 Runners References 3 Programming with runners 3.1 The user and kernel monads 3.2 Runners as a programming construct 4 A calculus for programming with runners 4.1 Types 4.2 Values and computations 4.3 Type system 4.4 Equational theory 5 Denotational semantics 5.1 Semantics of types 5.2 Semantics of values and computations 5.3 Coherence, soundness, and finalisation theorems 6 Runners in action 7 Implementation 8 Related work 9 Conclusion and future work 3 On the Versatility of Open Logical Relations 1 Introduction 2 The Playground 3 A Fundamental Gap 4 Warming Up: A Containment Theorem 5 Automatic Differentiation 6 On Refinement Types and Local Continuity 6.1 A Re nement Type System Ensuring Local Continuity 6.2 Basic Typing Rules 6.3 Typing Conditionals 6.4 Open-logical Predicates for Re nement Types 7 Related Work 8 Conclusion and Future Work References 4 Constructive Game Logic 1 Introduction 2 Related Work 3 Syntax 3.1 Example Games 4 Semantics 4.1 Realizers 4.2 Formula and Game Semantics 4.3 Demonic Semantics 5 Proof Calculus 6 Theory: Soundness 7 Operational Semantics 8 Theory: Constructivity 9 Conclusion and Future Work References 5 Optimal and Perfectly Parallel Algorithms forOn-demand Data-flow Analysis 1 Introduction 2 Preliminaries 2.1 The IFDS Framework 2.2 Trees and Tree Decompositions 3 Problem de nition 4 Treewidth-based Data-ow Analysis 4.1 Preprocessing 4.2 Word Tricks 4.3 Answering Queries 4.4 Parallelizability and Optimality 5 Experimental Results 6 Conclusion References 6 Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -5pt 1 Introduction 1.1 Correct Programs that Do Strange Things 1.2 Towards Simple Read-Only Speci cations for Synthesis 1.3 Our Contributions 2 Program Synthesis with Read-Only Borrows 2.1 Basics of SSL-based Deductive Program Synthesis 2.2 Reducing Non-Determinism with Read-Only Annotations 2.3 Composing Read-Only Borrows 2.4 Borrow-Polymorphic Inductive Predicates 2.5 Putting It All Together 3 BoSSL: Borrowing Synthetic Separation Logic 3.1 BoSSL rules 3.2 Memory Model 3.3 Soundness 4 Implementation and Evaluation 4.1 Experimental Setup 4.2 Performance and Quality of the Borrowing-Aware Synthesis 4.3 Stronger Correctness Guarantees 4.4 Robustness under Synthesis Perturbations 5 Limitations and Discussion 6 Related Work 7 Conclusion References 7 Soundness conditions for big-step semantics 1 Introduction 2 A meta-theory for big-step semantics 3 Extended semantics 3.1 Traces 3.2 Wrong 4 Expressing and proving soundness 4.1 Expressing soundness 4.2 Conditions ensuring soundness-must 4.3 Conditions ensuring soundness-may 5 Examples 5.1 Simply-typed -calculus with recursive types 5.2 MiniFJ&λ 5.3 Intersection and union types 5.4 MiniFJ&O 6 The partial evaluation construction 7 Related work 8 Conclusion and future work References 8 Liberate Abstract Garbage Collection fromthe Stack by Decomposing the Heap 1 Introduction 1.1 Examples 1.2 Generalizing the Approach 2 A-Normal Form λ- Calculus 3 Background 3.1 Semantic Domains 3.2 Concrete Semantics 3.3 Abstracting Abstract Machines with Garbage Collection 3.4 Stack-Precise CFA with Garbage Collection 3.5 The k-CFA Context Abstraction 4 From Threaded to Compositional Stores 4.1 Threaded-Store Semantics 4.2 Threaded-Store Semantics with Effect Log 4.3 Compositional-Store Semantics 4.4 Compositional-Store Semantics with Garbage Collection 5 Abstract Compositional-Store Semantics with Garbage Collection 6 Discussion 6.1 The Effects of Treating the Store Compositionally 6.2 The Effect of Treating the Time Compositionally 7 Related Work 8 Conclusion and Future Work References 9 SMT-Friendly Formalization of the Solidity Memory Model 1 Introduction 2 Background 2.1 Ethereum 2.2 Solidity 2.3 SMT-Based Programs 3 Formalization 3.1 Types 3.2 Local Storage Pointers 3.3 Contracts, State Variables, Functions 4 Evaluation 3.4 Statements 3.5 Assignments 3.6 Expressions 4 Evaluation 5 Related Work 6 Conclusion References 10 Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types 1 Introduction 2 Overview of our Approach 3 An MPST Theory with +, ∃ , and || 3.1 Types as Process Algebraic Terms 3.2 Global Types and Local Types 3.3 End-Point Projection: from Global Types to Local Types 3.4 Weak Bisimilarity of Global Types, Local Types, and Groups 3.5 Well-formedness of Global Types 3.6 Correctness of Projection under Well-Formedness 3.7 Decidability of Checking Well-Formedness 3.8 Discussion of Challenges 4 Practical Experience with the Theory 4.1 Implementation 4.2 Evaluation of the Approach 5 Related Work 6 Conclusion References 11 Verifying Visibility-Based Weak Consistency 1 Introduction 2 Weak Consistency 2.1 Weak-Visibility Speci ̇cations 2.2 Consistency againstWeak-Visibility Speci ̇cations 3 Establishing Consistency with Forward Simulation 3.1 Reducing Consistency to Safety Verification 3.2 Verifying Implementations 4 Proof Methodology 5 Implementation and Evaluation 6 RelatedWork 7 Conclusion and FutureWork A Appendix: Proofs to Theorems and Lemmas References 12 Local Reasoning for Global Graph Properties 1 Introduction 2 The Foundational Flow Framework 2.1 Preliminaries and Notation 2.2 Flows 2.3 Flow Graph Composition and Abstraction 3 Proof Technique 3.1 Encoding Flow-based Proofs in SL 3.2 Proof of the PIP 4 Advanced Flow Reasoning and the Harris List 4.1 The Harris List Algorithm 4.2 Product Flows for Reasoning about Overlays 4.3 Contextual Extensions and the Replacement Theorem 4.4 Existence and Uniqueness of Flows 4.5 Proof of the Harris List 5 Related Work 6 Conclusions and Future Work References 13 Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems 1 Introduction 2 The Core Concepts of Aneris 2.1 Local and Thread-Local Reasoning 2.2 Node-Local Reasoning 2.3 Example: An Addition Service 2.4 Example: A Lock Server 3 AnerisLang 4 The Aneris Logic 4.1 The Program Logic 4.2 Adequacy for Aneris 5 Case Study 1: A Load Balancer 6 Case Study 2: Two-Phase Commit 6.1 A Replicated Log 7 Related Work 8 Conclusion Bibliography 14 Continualization of Probabilistic ProgramsWith Correction 1 Introduction 2 Example 2.1 Continualization 2.2 Parameter Synthesis 2.3 Improving Inference 3 Syntax and Semantics of Programs 3.1 Source Language Syntax 3.2 Semantics 4 Continualizing Probabilistic Programs 4.1 Overview of the Algorithm 4.2 Distribution and Expression Transformations 4.3 Inuence Analysis and Control-Flow Correction of Predicates 4.4 Bringing it all together: Full Program Transformations 5 Synthesis of Continuity Correction Parameters 5.1 Optimization Framework 5.2 Optimization Algorithm 6 Methodology 6.1 Benchmarks 6.2 Experimental Setup 7 Evaluation 7.1 RQ1: Bene ts of Continualization 7.2 RQ2: Impact of Smoothing Factors 7.3 RQ3: Extending Results to Other Systems 8 Related Work 9 Conclusion References 15 Semantic Foundations for Deterministic Dataflow and Stream Processing 1 Introduction 2 Monoids as Types for Streams 3 Stream Transductions 4 Model of Computation 5 Combinators for Deterministic Dataow 6 Algebraic Reasoning for Optimizing Transformations 7 Related Work 8 Conclusion References 16 Connecting Higher-Order Separation Logic to a First-Order Outside World 1 Introduction 2 Background: Ghost State in Separation Logic 2.1 Ghost Algebras 2.2 Semantics of Ghost State 3 External State as Ghost State 4 Verifying C Programs with I/O in VST 5 Soundness of External-State Reasoning 6 Connecting VST to CertiKOS 6.1 CertiKOS Specifications 6.2 Relating OS and User State 6.3 Soundness of VST + CertiKOS 7 From syscall-level to hardware-level interactions 8 Related Work 9 Conclusion and Future Work References 17 Modular Inference of Linear Types for Multiplicity-Annotated Arrows 1 Introduction 2 Qualified-Typed Variant of λq→ 2.1 Syntax of Programs 2.2 Types 2.3 Typing Rules 2.4 Metatheories 3 Type Inference 3.1 Inference Algorithm 3.2 Entailment Checking by Horn SAT Solving 3.3 Issue: Inference of Ambiguous Types 4 Disambiguation by Quantifier Elimination 4.1 Elimination of Existential Quantifiers 4.2 Modified Typing Rules 5 Extension to Local Assumptions 5.1 “Let Should Not Be Generalized” for Our Case 5.2 Multiplicity of Let-Bound Variables 5.3 Inference Rule for Lets 5.4 Solving Constraints 6 Implementation and Evaluation 6.1 Implementation 6.2 Functions from Prelude 6.3 Performance Evaluation 7 Related Work 8 Conclusion References 18 RustHorn: CHC-based Verification for Rust Programs 1 Introduction 1.1 Challenges in Verifying Pointer-Manipulating Programs 1.2 Our Approach: Leverage Rust's Ownership System 2 Core Language: Calculus of Ownership and Reference 2.1 Syntax 2.2 Type System 2.3 Concrete Operational Semantics 3 CHC Representation of COR Programs 3.1 Multi-sorted Logic for Describing CHCs 3.2 Translation from COR Programs to CHCs 3.3 Correctness of the CHC Representation 3.4 Advanced Examples 3.5 Discussions 4 Implementation and Evaluation 4.1 Implementation of RustHorn 4.2 Benchmarks and Experiments 4.3 Experimental Results 5 Related Work 6 Conclusion References 19 A First-Order Logic with Frames 1 Introduction 2 Background: First-Order Logic with RecursiveDe nitions and Uninterpreted Combinations ofTheories 3 Frame Logic 3.1 Syntax of Frame Logic (FL) 3.2 Semantics of Support Expressions: Design Decisions 3.3 Formal Semantics of Frame Logic 3.4 A Frame Theorem 3.5 Reduction from Frame Logic to FO-RD 3.6 Expressing Data-Structures Properties in FL 4 Programs and Proofs 4.1 Operational Semantics 4.2 Triples and Validity 4.3 Program Logic 4.4 Weakest-Precondition Proof Rules 4.5 De nitions of MW Primitives 4.6 Example 5 Expressing a Precise Separation Logic 5.1 A Precise Separation Logic 5.2 Translation to Frame Logic 6 Discussion 7 Related Work 8 Conclusions Bibliography 20 Proving the safety of highly-available distributed objects 1 Introduction 2 Background 3 System Model 3.1 General Principles 3.2 Notations and Assumptions 3.3 Operational Semantics 3.4 Operational Semantics with State History 3.5 Correspondence between the semantics 4 Proving Invariants 4.1 Invariance Conditions 4.2 Applying the proof rule 4.3 Concurrency Control for Invariant Preservation 5 Case Studies 5.1 Consensus application 5.2 A replicated concurrency control 5.3 Courseware 6 Automation 6.1 Verification passes 7 Related Work 8 Conclusion Bibliography 21 Solving Program Sketches withLarge Integer Values 1 Introduction 2 Motivating Example 3 Preliminaries 4 Modular Arithmetic Semantics 4.1 The Chinese Remainder Theorem 4.2 The IMP-MOD Language 4.3 Equivalence between the two Semantics 5 From IMP to IMP-MOD Programs 5.1 Data Flow Analysis 5.2 From IMP to IMP-MOD 6 Solving IMP-MOD Sketches 6.1 Synthesis in IMP-MOD 7 Complexity of Rewritten Programs 7.1 Bit-complexity of Binary Encoding 7.2 Bit-complexity of Unary Encoding 7.3 Number of Required Primes 8 Evaluation 8.1 Benchmarks 8.2 Performance of Unary-p 8.3 Performance of Incremental Solving 8.4 Varying the Prime Number Set P 8.5 Size of SAT Formulas 9 Related Work References 22 Modular Relaxed Dependencies in Weak Memory Concurrency 23 ARMv8-A system semantics: instruction fetch in relaxed architectures 1 Introduction 2 Industry Practice and the Existing ARMv8-A Prose 3 Instruction Fetch Phenomena and Examples 3.1 Instruction-Fetch Atomicity 3.2 Coherence 3.3 Instruction Synchronisation 3.4 Multi-Copy Atomicity 3.5 Strength of the IC Instruction 3.6 Strength of the DC Instruction 4 An Operational Semantics for Instruction Fetch 5 An Axiomatic Semantics for Instruction Fetch 6 Validation 7 Related Work 8 Conclusion References 24 Higher-Ranked Annotation Polymorphic Dependency Analysis 1 Introduction 2 Intuition and motivation 3 The λ -calculus 4 The declarative type system 5 Metatheory 6 The type reconstruction algorithm 7 Implementation and Examples 8 Related Work 9 Conclusion and Future Work References 25 ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs 1 Introduction 2 Target Language 2.1 Syntax 2.2 Operational Semantics 3 Typing 3.1 Types and Contexts 3.2 Intraprocedural Type System 3.3 Interprocedural Fragment and Context-Sensitivity 3.4 Soundness 4 Inference and Extensions 4.1 Inference 4.2 Extensions 4.3 Limitations 5 Experiments 5.1 Results 6 Related Work 7 Conclusion Bibliography 26 Mixed Sessions 1 Introduction 2 There is Room for Mixed Sessions 2.1 Mixed Choices 2.2 Duplicated Labels in Choices for Types and for Processes 2.3 Unrestricted Output 3 The Syntax and Semantics of Mixed Sessions 3.1 Syntax 3.2 Operational Semantics 3.3 Typing 4 Well-typed Mixed Sessions Do Not Lead to Runtime Errors 5 Classical Sessions Were Mixed All Along 6 What is in the Way of a Compiler? 7 Related Work 8 Conclusion References 27 Higher-Order Spreadsheets with Spilled Arrays 1 Introduction 2 Challenges of Spilling 2.1 Design Principles for Spreadsheet Evaluation 2.2 Spill Collisions 2.3 Spill Cycles 3 Core Calculus for Spreadsheets 3.1 Syntax 3.2 Operational Semantics 4 Spill Calculus: Core Calculus with Spilled Arrays 4.1 Syntax 4.2 Spill Oracles and Iteration 4.3 Operational Semantics 4.4 Oracle Re nement 4.5 Technical Results 4.6 Limitations and Di erences with Real Systems 5 Grid Calculus: Spill Calculus with Sheets as Values 5.1 Extending Spreadsheets with Gridlets 5.2 Syntax and Operational Semantics 5.3 Formulas for Gridlets 6 Encoding Objects, Lambdas, and Functions 6.1 Encoding the Abadi and Cardelli Object Calculus 6.2 Encoding the Lambda Calculus 6.3 Encoding Sheet-De ned Functions 7 Related Work 8 Conclusion References Author Index This Open Access Book Constitutes The Proceedings Of The 29th European Symposium On Programming, Esop 2020, Which Took Place In Dublin, Ireland, In April 2020, And Was Held As Part Of The European Joint Conferences On Theory And Practice Of Software, Etaps 2020. The Papers Deal With Fundamental Issues In The Specification, Design, Analysis, And Implementation Of Programming Languages And Systems.