Logic-Based Program Synthesis and Transformation: 31st International Symposium, LOPSTR 2021, Tallinn, Estonia, September 7–8, 2021, Proceedings (Lecture Notes in Computer Science, 13290)

This book constitutes the refereed proceedings of the 31st International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2021, which was held during September 7-8, 2021.* The 8 papers presented in this volume were carefully reviewed and selected from a total of 15 reviewed submissions. Additionally, the book also contains 1 full-length invited talk. *Conference was held as a hybrid event due to the COVID-19 pandemic. Preface 6 Organization 8 Contents 10 String Abstract Domains and Their Combination 11 1 Introduction 11 2 Preliminaries 12 3 String Abstract Domains 13 3.1 Programming Language Agnostic String Abstract Domains 13 3.2 Language Specific String Domains 14 3.3 Regular Expression-Like Domains 15 3.4 The Class of Regular Languages as an Abstract Domain RL 16 4 Widening 16 5 Combining Domains 18 5.1 Direct Products 18 5.2 Reduced Products 19 5.3 Paraphrasing: Translating Approximate Information 19 5.4 One-on-One Paraphrasing 20 6 Reference Abstract Domains 21 7 Conclusion 24 References 24 Data Type Inference for Logic Programming 26 1 Introduction 26 2 Types 28 2.1 Semantics 30 2.2 Closed Types 31 3 Examples 32 4 Type System 34 5 Type Inference 37 5.1 Stratification 38 5.2 Constraints and Constraint Generation 38 5.3 Constraint Solving 40 5.4 Decidability 43 5.5 Soundness 43 6 Related Work 44 7 Final Remarks 45 References 45 Automating the Functional Correspondence Between Higher-Order Evaluators and Abstract Machines 48 1 Introduction 48 2 Interpreters and the Meta-language 50 3 Transformation 52 3.1 Administrative Normal Form 52 3.2 Control-Flow Analysis 53 3.3 Selective CPS Transformation 57 3.4 Selective Defunctionalization 59 4 Case Studies 60 5 Conclusion 62 A A Primer on the Functional Correspondence 63 B Normalization by Evaluation for -calculus 64 References 67 S-Semantics–an Example 70 1 Introduction 70 2 S-semantics 71 3 The n Queens Program 74 4 Correctness of nqueens 76 4.1 Specification for Correctness 76 4.2 Correctness Proof for nqueens 78 5 Completeness 80 5.1 Specification for Completeness 80 5.2 Completeness Proof 81 6 Comments 82 7 Summary 83 References 84 Disjunctive Delimited Control 85 1 Introduction 85 2 Overview and Motivation 86 2.1 Background: Conjunctive Delimited Control 86 2.2 Delimited Continuations with Disjunction 88 3 Meta-interpreter Semantics 90 3.1 Core Interpreter 90 4 Case Studies 93 4.1 Branch-and-Bound: Nearest Neighbour Search 93 4.2 Probabilistic Programming 95 5 Properties of the Meta-interpreter 97 6 Related Work 98 7 Conclusion and Future Work 100 References 100 Towards Substructural Property-Based Testing 102 1 Introduction 102 2 A Motivating Example 104 3 A Primer on Linear Logic Programming 105 4 The Proof-Theory of PBT 109 5 Case Study 112 5.1 On Linear Encodings 113 5.2 Experimental Evaluation 115 6 Related Work and Conclusions 118 References 119 The Next 700 Program Transformers 123 1 Introduction 123 2 Language 125 3 Process Trees 127 4 A Hierarchy of Program Transformers 133 4.1 Level 0 Transformer 134 4.2 Level k+1 Transformers 134 5 Examples 136 6 Speedups 138 7 Termination 140 8 Related Work 141 9 Conclusion and Further Work 142 References 143 Representation and Processing of Instantaneous and Durative Temporal Phenomena 145 1 Introduction 145 2 Language 146 2.1 Syntax 147 2.2 Grammar 148 2.3 Semantics 149 3 Maritime Use Case Examples 151 3.1 Stopped Vessel 152 3.2 Moored Vessel 152 3.3 Vessel Trips 153 3.4 Fishing Trips 153 4 Executable Semantics 153 4.1 Stream Processing 154 4.2 Processing of Temporal Phenomena 158 5 Implementation 160 5.1 Architecture 160 5.2 Empirical Evaluation 161 6 Related Work 163 7 Summary and Future Directions 164 References 164 Prefix-Based Tracing in Message-Passing Concurrency 167 1 Introduction 167 2 A Message-Passing Concurrent Language 169 3 Prefix-Based Tracing Semantics 173 4 A Program Instrumentation for Prefix-Based Tracing 179 5 Concluding Remaks 184 References 184 Author Index 186