LEADER 05061nam 2200457 450 001 996464451403316 005 20231110220320.0 010 $a3-030-98869-4 035 $a(MiAaPQ)EBC6921855 035 $a(Au-PeEL)EBL6921855 035 $a(CKB)21393292300041 035 $a(PPN)261518224 035 $a(EXLCZ)9921393292300041 100 $a20221018d2022 uy 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 00$aLogic-based program synthesis and transformation $e31st International Symposium, LOPSTR 2021, Tallinn, Estonia, September 7-8, 2021, proceedings /$fedited by Emanuele De Angelis, Wim Vanhoof 210 1$aCham, Switzerland :$cSpringer,$d[2022] 210 4$dİ2022 215 $a1 online resource (186 pages) 225 1 $aLecture Notes in Computer Science ;$vv.13290 311 08$aPrint version: De Angelis, Emanuele Logic-Based Program Synthesis and Transformation Cham : Springer International Publishing AG,c2022 9783030988685 320 $aIncludes bibliographical references and index. 327 $aIntro -- 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. 327 $a2.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. 410 0$aLecture Notes in Computer Science 606 $aComputer logic$vCongresses 615 0$aComputer logic 676 $a005.115 702 $aVanhoof$b Wim 702 $aDe Angelis$b Emanuele 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996464451403316 996 $aLogic-Based Program Synthesis and Transformation$92914320 997 $aUNISA