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

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