Foundations of Software Science and Computation Structures 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, P

The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. ETAPS Foreword Preface Organization Contents Constructing a universe for the setoid model 1 Introduction 1.1 Related work 2 MLTT^Prop 2.1 Formalization 3 Setoid model 3.1 Setoid model as a CwF 3.2 Setoid Type Theory 4 Universe of setoids 4.1 Inductive-recursive universes 4.2 Inductive-recursive setoid universe 4.3 Inductive-inductive setoid universe 4.4 Inductive setoid universe 5 Conclusions and further work References Nominal Equational Problems 1 Introduction 2 Background 3 Nominal Equational Problems 4 A rule-based procedure 4.1 Simplification Rules 4.2 Soundness and Preservation of Solutions 4.3 Termination 5 Nominal Equational Solved Forms 6 Conclusion References Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy 1 Introduction 2 Preliminaries 3 The cut-off problem for acyclic Petri nets 3.1 Characterizing acyclic systems with cut-offs 3.2 Polynomial time algorithm 4 The Scaling and Insertion lemmas 4.1 The Scaling Lemma 4.2 The Insertion Lemma 5 Polynomial time algorithm for the general case 5.1 Characterizing systems with cut-offs 5.2 Polynomial time algorithm 6 Symmetric rendez-vous protocols 7 Symmetric protocols with leaders 7.1 A non-deterministic polynomial time algorithm References Fixpoint Theory – Upside Down 1 Introduction 2 Lattices and MV-Algebras 3 Non-expansive Functions and Their Approximations 4 Proof Rules 5 (De)Composing Functions and Approximations 6 Applications 6.1 Termination Probability 6.2 Behavioural Metrics for Probabilistic Automata 6.3 Bisimilarity 7 Simple Stochastic Games 8 Conclusion References "Most of'' leads to undecidability: Failure of adding frequencies to LTL 1 Introduction 1.1 Related work 2 Preliminaries 3 Playing with Half Operator 4 Undecidability of LTL extensions 4.1 “Half of” meets the halting problem Fact 5 Fact 6 6.1 Undecidability of model-checking 6.2 Most-Frequent Letter and Undecidability 6.3 Most-Frequent Letter: the reduction 7 Decidable variants 8 Two-Variable First-Order Logic with Majority 9 Conclusions References Combining Semilattices and Semimodules 1 Introduction 2 (Weak) Distributive laws 3 The Powerset and Semimodule Monads 4 The Weak Distributive Law δ : SP → PS 5 The Weak Lifting of P to EM(S) 5.1 Proof of Theorem 24 6 The Composite Monad: an Algebraic Presentation 7 Conclusions: Related and Future Work References One-way Resynchronizability of Word Transducers 1 Introduction 2 Preliminaries 3 One-way resynchronizability 3.1 Regular resynchronizers 3.2 Main result 4 Proof overview for Theorem 1 4.1 Flows and inversions 4.2 Dominant output intervals 5 Proof of Theorem 1 6 Proof overview of Theorem 2 7 Complexity 8 Conclusions References Fair Refinement for Asynchronous Session Types 1 Introduction 2 Refinement for Asynchronous Session Types 2.1 Preliminaries: Asynchronous Session Types 2.2 Fair Refinement for Asynchronous Session Types 2.3 Controllability for Asynchronous Session Types 3 Fair Asynchronous Session Subtyping 4 A Sound Algorithm for Fair Asynchronous Subtyping 5 Implementation 6 Related and Future Work References Running Time Analysis of Broadcast Consensus Protocols 1 Introduction 2 Preliminaries 3 Example: Majority 4 Comparison with other Models 4.1 Non-Deterministic Broadcast Protocols 4.2 Population Protocols 5 Protocols for Presburger Arithmetic 5.1 Linear Inequalities 5.2 Modulo Predicates and Boolean Combinations 6 Protocols for all Predicates in ZPL References Leafy automata for higher-order concurrency 1 Introduction 2 Finitary Idealized Concurrent Algol (FICA) 3 Game semantics 4 Leafy automata 5 Local leafy automata (LLA) 6 From FICA to LA 7 Local FICA 8 From LA to FICA 9 Conclusion and further work References Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic 1 Introduction 2 Background in Abstract Rewriting 3 λ-calculi: CbN, CbV, and bang 3.1 Call-by-Name and Call-by-Value λ-calculi 3.2 Bang calculi 3.3 CbN and CbV translations into the bang calculus 4 The least-level strategy 4.1 Least-level reduction in bang calculi 4.2 Least-level for a bang calculus: examples. 4.3 Least-level for CbN and CbV λ-calculi 5 Embedding of CbN and CbV by level 6 Least-level factorization via bang calculus 6.1 Factorization of →β! in a bang calculus 6.2 Pure calculi and least-level normalization 6.3 Least-level Factorization, Modularly 7 Case study: non-deterministic λ-calculi 8 Conclusions and Related Work References Generalized Bounded Linear Logic and its Categorical Semantics 1 Introduction 2 Generalized Bounded Linear Logic 2.1 Indexing 2-Category 2.2 Formulas and Proofs 2.3 Complexity of Cut-Elimination in GBLL 3 Translation from Constrained BLL 3.1 Resource Polynomials and Constraints 3.2 Formulas and Inference Rules of CBLL 3.3 Translation into GBAL+ 4 Categorical Semantics for GBLL 4.1 Semantics of GBLL 4.2 Construction of an Indexed Linear Exponential Comonad 4.3 GBLL Semantics by Realizability Category 5 Conclusion and Related Work References Focused Proof-search in the Logic of Bunched Implications 1 Introduction 2 Re-presentations of BI 2.1 Traditional Syntax 2.2 Sequent Calculus 2.3 Nested Calculus 3 A Focused System 3.1 Polarisation 3.2 Focused Calculus 3.3 Completeness of fBI 4 Conclusion References Interpolation and Amalgamation for Arrays with MaxDiff 1 Introduction 2 Formal Preliminaries 3 Arrays with MaxDiff 3.1 Our roadmap 4 Embeddings 5 Amalgamation 6 Satisfiability 7 An interpolation algorithm 8 When indexes are just a total order 9 Conclusions and further work References Adjoint Reactive GUI Programming Introduction The Language Formal Calculus Semantics Related and Future Work References On the Expressiveness of Büchi Arithmetic 1 Introduction 2 Preliminaries 3 The inexpressiveness of existential Büchi arithmetic 4 Expressive completeness of the ∑2-fragment of Büchi arithmetic 5 Existential Büchi arithmetic defines regular languages of polynomial growth 6 Conclusion References Parametricity for Primitive Nested Types 1 Introduction 2 The Calculus 2.1 Types 2.2 Terms 3 Interpreting Types 3.1 Interpreting Types as Sets 3.2 Interpreting Types as Relations 4 The Identity Extension Lemma 5 Interpreting Terms 6 Free Theorems for Nested Types 6.1 Consequences of Naturality 6.2 The Abstraction Theorem 7 Conclusion and Directions for Future Work References The Spirit of Node Replication 1 Introduction 2 A Calculus for Node Replication 3 Operational Properties 4 Encoding Evaluation Strategies 4.1 Call-by-name 4.2 Call-by-need 5 A Type System for the λR-calculus 6 Observational Equivalence 7 Related Works and Conclusion References Nondeterministic and co-Nondeterministic Implies Deterministic, for Data Languages 1 Introduction 2 Data languages and register automata 3 Examples 4 Main results 5 Orbit-finite automata 6 Proof of Theorem 1 6.1 Examples 6.2 Proof of Lemma 1 7 Application to Unambiguous Register Automata 8 Proof of Theorem 2 9 Final remarks References Certifying Inexpressibility 1 Introduction 2 Preliminaries 2.1 Transducers and Realizability 2.2 Automata 3 Refuting DBW-Recognizability 3.1 Complexity 3.2 Certifying DBW-Refutation 4 Separability and Approximations 4.1 Refuting Separability 4.2 Certificate-Guided Approximation 5 Other Classes of Deterministic Automata 6 Discussion and Directions for Future Research References A General Semantic Construction of Dependent Refinement Type Systems, Categorically 1 Introduction 2 Preliminaries 3 Lifting SCCompCs and Fibred Coproducts 3.1 Lifting SCCompCs 3.2 Lifting Fibred Coproducts 4 Lifting Monads on SCCompCs 5 Soundness 5.1 Underlying Type System 5.2 Predicate Logic 5.3 Refinement Type System 5.4 Semantics 6 Toward Recursion in Refinement Type Systems 6.1 Conway Operators 6.2 Recursion in the Underlying Type System 7 Related Work 8 Conclusion and Future Work References Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP 1 Introduction 2 Preliminaries 3 Characterizing Energy-Parity via Gain and Bailout 4 Bailout 5 Gain 6 The Main Results 7 Conclusion and Outlook References Nondeterministic Syntactic Complexity 1 Introduction 2 Preliminaries 3 Duality Theory of Semilattice Automata 4 Boolean Representations and Subatomic NFAs 5 Applications 5.1 Unary languages 5.2 Languages with a canonical state-minimal nfa 6 Conclusion and Future Work References A String Diagrammatic Axiomatisation of Finite-State Automata 1 Introduction 2 Syntax and semantics 3 Equational theory 4 Encoding regular expressions and automata 4.1 From regular expressions to string diagrams 4.2 From automata to string diagrams... 4.3 ...and back 4.4 Interlude: from regular to context-free languages 5 Completeness and Determinisation 5.1 Determinisation 5.2 Minimisation and completeness 6 Discussion References Work-sensitive Dynamic Complexity of Formal Languages 1 Introduction 2 Preliminaries 3 Work-sensitive Dynamic Complexity 3.1 The Dynamic Complexity Framework 3.2 A syntax for work-efficient dynamic programs 3.3 Implementing Procedural-DynFO-programs as PRAMs 4 A simple work-efficient Dynamic Program 5 Regular Languages 5.1 DynFO-programs with sublinear work for regular languages 5.2 DynFO-programs with polylogarithmic work for star-free languages 6 Context Free Languages 6.1 A conditional lower bound for context-free languages 6.2 On work-efficient dynamic programs for Dyck languages 7 Conclusion References Learning Pomset Automata 1 Introduction 2 Pomset Recognisers 3 Learning Pomset Recognisers 3.1 Observation Table 3.2 The Learning Algorithm 3.3 Termination and Query Complexity 3.4 Minimality of Hypotheses 4 Conversion to Pomset Automata 5 Discussion References The Structure of Sum-Over-Paths, its Consequences, and Completeness for Clifford 1 Introduction 2 Background 2.1 PROPs and String Diagrams 2.2 †-Compact PROPs 2.3 Example: Qubit 3 The Category SOP 3.1 SOP as a PROP 3.2 From SOP to Qubit 3.3 SOP as a †-Compact PROP 4 Redefinition of SOP 5 SOP and Graphical Languages 5.1 The Cliffrord Fragment of the ZH-Calculus 5.2 From ZH_Clif to SOP 5.3 The Clifford Fragment of SOP 5.4 From SOP_Clif to ZH_Clif 6 A Complete Rewrite System for Clifford 7 SOP with Discards 7.1 The Discard Construction on SOP 7.2 SOP with Discards for Clifford References A Quantified Coalgebraic van Benthem Theorem 1 Introduction 2 Preliminaries 3 Quantale-Valued Distances and Lax Extensions 4 Quantale-Valued Modal and Predicate Logics 5 Behavioural Distance and Quantitative Bisimulation Invariance 6 Modal Approximation 7 Locality and Modal Characterization 8 Conclusions References Author Index This open access book constitutes the proceedings of the 24th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 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 28 regular papers presented in this volume were carefully reviewed and selected from 88 submissions. They deal with research on theories and methods to support the analysis, integration, synthesis, transformation, and verification of programs and software systems.