Programming Languages and Systems

Description

This open access book constitutes the proceedings of the 30th European Symposium on Programming, ESOP 2021, which was held during March 27 until April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The 24 papers included in this volume were carefully reviewed and selected from 79 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems. ETAPS Foreword Preface Organization Contents The Decidability of Verification under PS 2.0 1 Introduction 2 Preliminaries 3 The Promising Semantics 4 Undecidability of Consistent Reachability in PS 2.0 5 Decidable Fragments of PS 2.0 5.1 Formal Model of LoHoW 5.2 Decidability of LoHoW with Bounded Promises 6 Source to Source Translation 6.1 Translation Maps 7 Implementation and Experimental Results 8 Related Work and Conclusion References Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains 1 Introduction 1.1 Motivating Example: Leader election 1.2 Challenges in property checking 1.3 Our Contributions 2 Background and Terminology 2.1 Modeling of Asynchronous Message Passing Systems as VCFGs 2.2 Data flow analysis over iVCFGs 3 Backward DFAS Approach 3.1 Assumptions and Definitions 3.2 Properties of Demand and Covering 3.3 Data Flow Analysis Algorithm 3.4 Illustration 3.5 Properties of the algorithm 4 Forward DFAS Approach 5 Implementation and Evaluation 5.1 Benchmarks and modeling 5.2 Data flow analysis results 5.3 Limitations and Threats to Validity 6 Related Work 7 Conclusions and Future Work References Types for Complexity of Parallel Computation in Pi-Calculus 1 Introduction 2 The Pi-calculus with Semantics for Work and Span 2.1 Syntax, Congruence and Standard Semantics for π-Calculus 2.2 Semantics and Complexity 2.3 An Example Process 3 Size Types for the Work 3.1 Size Input/Output Types 3.2 Subject Reduction 4 Types for Parallel Complexity 4.1 Size Types with Time 4.2 Examples 4.3 Complexity Results 5 An Example: Bitonic Sort 6 Related Work 7 Perspectives Acknowledgements References Checking Robustness Between Weak Transactional Consistency Models-5pt 1 Introduction 2 Overview 3 Consistency Models 3.1 Robustness 4 Robustness Against CC Relative to PC 5 Robustness Against PC Relative to SI 6 Proving Robustness Using Commutativity DependencyGraphs 7 Experimental Evaluation 8 Related Work References Verified Software Units 1 Introduction 2 Program verification using VST 3 VSU calculus 3.1 Components and soundness 3.2 Derived rules 4 APDs and specification interfaces 4.1 Abstract predicate declarations (APDs) 4.2 Abstract specification interfaces (ASIs) 4.3 Verification of ASI-specified compilation units 4.4 A VSU for a malloc-free library 4.5 Putting it all together 5 Modular verification of the Subject/Observer pattern 5.1 Specification and proof reuse 5.2 Pattern-level specification 6 Verification of object principles 7 Discussion References An Automated Deductive Verification Framework for Circuit-building Quantum Programs 1 Introduction 1.1 Quantum computing 1.2 The hybrid model. 1.3 The problem with quantum algorithms. 1.4 Goal and challenges. 1.5 Proposal. 1.6 Contributions. 1.7 Discussion. 2 Background: Quantum Algorithms and Programs 2.1 Quantum data manipulation. 2.2 Quantum circuits. 2.3 Reasoning on circuits and the matrix semantics. 2.4 Path-sum representation. 3 Introducing PPS 3.1 Motivating example. 3.2 Parametrizing path-sums. 4 Qbricks-DSL 4.1 Syntax of Qbricks-DSL. 4.2 Operational semantics. 4.3 Properties. 4.4 Universality and usability of the chosen circuit constructs. 4.5 Validity of circuits. 4.6 Denotational semantics. 5 Qbricks-Spec 5.1 Syntax of Qbricks-Spec. 5.2 The types pps and ket. 5.3 Denotational semantics of the new types. 5.4 Regular sequents in Qbricks-Spec. 5.5 Parametricity of PPS. 5.6 Standard matrix semantics and correctness of PPS semantics. 6 Reasoning on Quantum Programs 6.1 HQHL judgments. 6.2 Deduction rules for term constructs. 6.3 Deduction rules for pps. 6.4 Equational reasoning. 6.5 Additional deductive rules. 7 Implementation 8 Case studies and experimental evaluation 8.1 Examples of formal specifications. 8.2 Experimental evaluation. 8.3 Prior verification efforts. 8.4 Evaluation: benefits of PPS and Qbricks. 9 Related works 10 Conclusion Acknowledgments. References Nested Session Types 1 Introduction 2 Overview of Nested Session Types 3 Description of Types 4 Type Equality 4.1 Type Equality Definition 4.2 Decidability of Type Equality 5 Practical Algorithm for Type Equality 5.1 Type Equality Declarations 6 Formal Language Description 6.1 Basic Session Types 6.2 Type Safety 7 Relationship to Context-Free Session Types 8 Implementation 9 More Examples 10 Further Related Work 11 Conclusion References Coupled Relational Symbolic Execution for Differential Privacy 1 Introduction 2 CRSE Informally 3 Preliminaries 4 Concrete languages 4.1 PFOR 4.2 RPFOR 5 Symbolic languages 5.1 SPFOR 5.2 SRPFOR 6 Metatheory 7 Strategies for counterexample finding 8 Examples 9 Related Works 10 Conclusion References Graded Hoare Logic and its Categorical Semantics 1 Introduction 2 Overview of GHL and Prospectus of its Model 3 Loop Language and Graded Hoare Logic 3.1 Preliminaries 3.2 The Loop Language 3.3 Assertion Logic 3.4 Graded Hoare Logic 3.5 Example Instantiations of GHL 4 Graded Categories 4.1 Homogeneous Coproducts in Graded Categories 4.2 Graded Freyd Categories with Countable Coproducts 4.3 Semantics of The Loop Language in Freyd Categories 5 Modelling Graded Hoare Logic 5.1 Interpretation of the Assertion Logic using Fibrations 5.2 Interpretation of Graded Hoare Logic 5.3 Instances of Graded Hoare Logic 6 Related Work 7 Conclusion References Do Judge a Test by its Cover 1 Introduction 2 Classical Combinatorial Testing 3 Generalizing Coverage 4 Sparse Test Descriptions 4.1 Encoding “Eventually” 4.2 Defining Coverage 5 Thinning Generators with QuickCover 5.1 Online Generator Thinning 6 Evaluation 6.1 Case Study: Normalization Bugs in System F 6.2 Case Study: Strictness Analysis Bugs in GHC 7 Related Work 7.1 Generalizations of Combinatorial Testing 7.2 Comparison with Enumerative Property-Based Testing 7.3 Comparison with Fuzzing Techniques 8 Conclusion and Future Work 8.1 Variations 8.2 Combinatorial Coverage of More Types 8.3 Regular Tree Expressions for Directed Generation Acknowledgments References For a Few Dollars More 1 Introduction 2 Specification of Algorithms With Resources 2.1 Nondeterministic Computations With Resources 2.2 Atomic Operations and Control Flow 2.3 Refinement on NREST 2.4 Refinement Patterns 3 LLVM With Cost Semantics 3.1 Basic Monad 3.2 Shallowly Embedded LLVM Semantics 3.3 Cost Model 3.4 Reasoning Setup 3.5 Primitive Setup 4 Automatic Refinement 4.1 Heap nondeterminism refinement 4.2 The Sepref Tool 4.3 Extracting Hoare Triples 4.4 Attain Supremum 5 Case Study: Introsort 5.1 Specification of Sorting 5.2 Introsort’s Idea 5.3 Quicksort Scheme 5.4 Final Insertion Sort 5.5 Separating Correctness and Complexity Proofs 5.6 Refining to LLVM 5.7 Benchmarks 6 Conclusions 6.1 Related Work 6.2 Future Work References Run-time Complexity Bounds Using Squeezers 1 Introduction 2 Overview 3 Complexity Analysis based on Squeezers 3.1 Time complexity as a function of rank 3.2 Complexity decomposition by partitioned simulation 3.3 Extraction of recurrence relations over ranks 3.4 Establishing the requirements of the recurrence relations extraction 3.5 Trace-length vs. state-size recurrences with squeezers 4 Synthesis 4.1 SyGuS 4.2 Verification 5 Empirical Evaluation 5.1 Experiments 5.2 Case study: Subsets example 6 Related Work 7 Conclusion Acknowledgements. References Complete trace models of state and control 1 Introduction 2 HOSC 3 HOSC[HOSC] 3.1 Names and abstract values 3.2 Actions and traces 3.3 Extended syntax and reduction 3.4 Configurations 3.5 Transitions 3.6 Correctness and full abstraction 4 GOSC[HOSC] 5 HOS[HOSC] 6 GOS[HOSC] 7 Concluding remarks 8 Related Work References Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols 1 Introduction 2 Session Types 3 Session Coalgebra 3.1 Alternative Presentation of Session Coalgebras 3.2 Coalgebra of Session Types 4 Type Equivalence, Duality and Subtyping 4.1 Bisimulation 4.2 Duality 4.3 Parallelizability 4.4 Simulation and Subtyping 4.5 Decidability 5 Typing Rules 5.1 A Session π-calculus 5.2 Typing Rules 6 Algorithmic Type Checking 7 Concluding Remarks References Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages 1 Introduction 2 A Motivating Example from Phylogenetics 3 A Calculus for Probabilistic Programming Languages 3.1 Syntax 3.2 Semantics 3.3 Resampling Semantics 4 The Target Measure of a Program 4.1 A Measure Space over Traces 4.2 A Measurable Space over Terms 5 Formal SMC 5.1 Preliminaries: Transition Kernels 5.2 Algorithm 5.3 Correctness 6 Formal SMC for Probabilistic Programming Languages 6.1 The Sequence of Measures Generated by a Program 6.2 Correctness 7 SMC Algorithms 7.1 The Bootstrap Particle Filter 7.2 Other SMC Algorithms 8 Related Work 9 Conclusions Acknowledgments References Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere 1 Introduction 2 Probabilistic Programming and Trace-Based Inference 2.1 Measures and Densities 2.2 Probabilistic Programming: a (Running) Example 2.3 Gradient-Based Approximate Inference 3 Sampling Semantics for Statistical PCF 3.1 Statistical PCF 3.2 Operational Semantics 4 Differentiability of the Weight and Value Functions 4.1 Background on Differentiable Functions 4.2 Why Almost Everywhere Differentiability Can Fail 4.3 Admissible Primitive Functions 4.4 Almost Sure Termination 5 Stochastic Symbolic Execution 5.1 Symbolic Terms and Values 5.2 Symbolic Operational Semantics 6 Densities of Almost Surely Terminating Programs areDifferentiable Almost Everywhere 6.1 Differentiability on Terminating Traces 6.2 Differentiability for Almost Surely Terminating Terms 7 Conclusion References Graded Modal Dependent Type Theory 1 Introduction 2 GrTT: Graded Modal Dependent Type Theory 2.1 Syntax 2.2 Typing Judgments, Contexts, and Grading 2.3 Typing Rules 2.4 Operational Semantics 2.5 Implementation and Examples 3 Case Studies 3.1 Recovering Martin-L¨of Type Theory 3.2 Determining Usage via Quantitative Semirings 3.3 Simply-typed Reasoning 3.4 Recovering Parametricity via Grading 3.5 Graded Modal Types and Non-dependent Linear Types 4 Metatheory 4.1 Substitution 4.2 Type Preservation 4.3 Structural Rules 4.4 Strong Normalization 5 Implementation 6 Discussion References Automated Termination Analysis of Polynomial Probabilistic Programs 1 Introduction 2 Preliminaries 2.1 Programming Model: Prob-Solvable Loops 2.2 Canonical Probability Space 2.3 Martingales 3 Proof Rules for Probabilistic Termination 3.1 Positive Almost Sure Termination (PAST) 3.2 Almost Sure Termination (AST) 3.3 Non-Termination 4 Relaxed Proof Rules for Probabilistic Termination 5 Algorithmic Termination Analysis through Asymptotic Bounds 5.1 Prob-solvable Loops and Monomials 5.2 Computing Asymptotic Bounds for Prob-solvable Loops 5.3 Algorithms for Termination Analysis of Prob-solvable Loops 5.4 Ruling out Proof Rules for Prob-Solvable Loops 6 Implementation and Evaluation 6.1 Implementation 6.2 Experimental Setting and Results 7 RelatedWork 8 Conclusion Bayesian strategies: probabilistic programs as generalised graphical models 1 Introduction 1.1 From Bayesian networks to Bayesian strategies 1.2 Our approach 2 Probability distributions, Bayesian networks, andprobabilistic programming 2.1 Probability and measure 2.2 Bayesian networks 2.3 A language for probabilistic modelling 3 Programs as event structures 3.1 Control flow, data flow, and probability 3.2 Branching 3.3 Programs with free variables 3.4 Higher-order programs 3.5 Bayesian event structures 3.6 Symmetry 4 Games and Bayesian strategies 4.1 An introduction to game semantics based on event structures 4.2 Composition of strategies 5 A denotational model 5.1 Categorical structure 5.2 Denotational semantics 6 Conclusion and perspectives References Temporal Refinements for Guarded Recursive Types 1 Introduction 2 Outline 3 The Pure Calculus 4 A Temporal Modal Logic 5 A Temporally Refined Type System 6 The Full System 7 Semantics 8 Examples 9 Related Work 10 Conclusion and Future Work References Query Lifting 1 Introduction 2 Overview 3 Background 4 A relational calculus of tabular functions 4.1 Semantics and translation to NRCλ(Set, Bag) 5 Delateralization 6 Query lifting and shredding 6.1 Reflecting shredded queries into NRCλ(Set, Bag) 6.2 The stitching function 7 Related work 8 Conclusions References Reverse AD at Higher Types: Pure, Principled and Denotationally Correct 1 Introduction 2 Key Ideas 3 λ-Calculus as a Source Language for AD 4 Linear λ-Calculus as an Idealised AD Target Language 5 Semantics of the Source and Target Languages 5.1 Preliminaries 5.2 Abstract Semantics 5.3 Concrete Semantics 6 Pairing Primals with Tangents/Adjoints, Categorically 6.1 Grothendieck Constructions on Strictly Indexed Categories 6.2 Structure of ΣCL and ΣCLop for Locally Indexed Categories 7 Novel AD Algorithms as Source-Code Transformations 8 Proving Reverse and Forward AD Semantically Correct 8.1 Preliminaries 8.2 Subsconing for Correctness of AD 9 Practical Relevance and Implementation 10 Related and Future Work Acknowledgements References Sound and Complete Concolic Testingfor Higher-order Functions 1 Introduction 2 Higher-order Concolic Testing by Example 2.1 First-Order Concolic Execution in a Nutshell 2.2 From Numbers to Function Inputs 2.3 Input Interactions 2.4 Blind Extensions Are Not Enough 2.5 Higher-order Inputs 3 Formalizing Higher-order Concolic Testing 3.1 From User Programs to Concolic Evaluation 3.2 Evolution of Higher-order Inputs 3.3 Adding Concretization 4 Correctness of Higher-order Concolic Testing 5 From the Model to a Proof-of-Concept Implementation 6 Related Work 7 Conclusion Acknowledgments References Strong-Separation Logic 1 Introduction 2 Strong- and Weak-Separation Logic 2.1 Preliminaries 2.2 Two Semantics of Separation Logic 2.3 Correspondence of Strong and Weak Semantics on Positive Formulas 3 Deciding the SSL Satisfiability Problem 3.1 Memory Chunks 3.2 Abstract Memory States 3.3 The Refinement Theorem for SSL 3.4 Recursive Equations for Abstract Memory States 3.5 Refining the Refinement Theorem: Bounding Garbage 3.6 Deciding SSL by AMS Computation 3.7 Complexity of the SSL Satisfiability Problem 4 Program Verification with Strong-Separation Logic 5 Normal Forms and the Abduction Problem 6 Conclusion References Author Index