Logic-Based Program Synthesis and Transformation : 31st International Symposium, LOPSTR 2021, Tallinn, Estonia, September 7–8, 2021, Proceedings

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 Organization Contents String Abstract Domains and Their Combination 1 Introduction 2 Preliminaries 3 String Abstract Domains 3.1 Programming Language Agnostic String Abstract Domains 3.2 Language Specific String Domains 3.3 Regular Expression-Like Domains 3.4 The Class of Regular Languages as an Abstract Domain RL 4 Widening 5 Combining Domains 5.1 Direct Products 5.2 Reduced Products 5.3 Paraphrasing: Translating Approximate Information 5.4 One-on-One Paraphrasing 6 Reference Abstract Domains 7 Conclusion References Data Type Inference for Logic Programming 1 Introduction 2 Types 2.1 Semantics 2.2 Closed Types 3 Examples 4 Type System 5 Type Inference 5.1 Stratification 5.2 Constraints and Constraint Generation 5.3 Constraint Solving 5.4 Decidability 5.5 Soundness 6 Related Work 7 Final Remarks References Automating the Functional Correspondence Between Higher-Order Evaluators and Abstract Machines 1 Introduction 2 Interpreters and the Meta-language 3 Transformation 3.1 Administrative Normal Form 3.2 Control-Flow Analysis 3.3 Selective CPS Transformation 3.4 Selective Defunctionalization 4 Case Studies 5 Conclusion A A Primer on the Functional Correspondence B Normalization by Evaluation for -calculus References S-Semantics–an Example 1 Introduction 2 S-semantics 3 The n Queens Program 4 Correctness of nqueens 4.1 Specification for Correctness 4.2 Correctness Proof for nqueens 5 Completeness 5.1 Specification for Completeness 5.2 Completeness Proof 6 Comments 7 Summary References Disjunctive Delimited Control 1 Introduction 2 Overview and Motivation 2.1 Background: Conjunctive Delimited Control 2.2 Delimited Continuations with Disjunction 3 Meta-interpreter Semantics 3.1 Core Interpreter 4 Case Studies 4.1 Branch-and-Bound: Nearest Neighbour Search 4.2 Probabilistic Programming 5 Properties of the Meta-interpreter 6 Related Work 7 Conclusion and Future Work References Towards Substructural Property-Based Testing 1 Introduction 2 A Motivating Example 3 A Primer on Linear Logic Programming 4 The Proof-Theory of PBT 5 Case Study 5.1 On Linear Encodings 5.2 Experimental Evaluation 6 Related Work and Conclusions References The Next 700 Program Transformers 1 Introduction 2 Language 3 Process Trees 4 A Hierarchy of Program Transformers 4.1 Level 0 Transformer 4.2 Level k+1 Transformers 5 Examples 6 Speedups 7 Termination 8 Related Work 9 Conclusion and Further Work References Representation and Processing of Instantaneous and Durative Temporal Phenomena 1 Introduction 2 Language 2.1 Syntax 2.2 Grammar 2.3 Semantics 3 Maritime Use Case Examples 3.1 Stopped Vessel 3.2 Moored Vessel 3.3 Vessel Trips 3.4 Fishing Trips 4 Executable Semantics 4.1 Stream Processing 4.2 Processing of Temporal Phenomena 5 Implementation 5.1 Architecture 5.2 Empirical Evaluation 6 Related Work 7 Summary and Future Directions References Prefix-Based Tracing in Message-Passing Concurrency 1 Introduction 2 A Message-Passing Concurrent Language 3 Prefix-Based Tracing Semantics 4 A Program Instrumentation for Prefix-Based Tracing 5 Concluding Remaks References Author Index