Foundations of Software Science and Computation Structures : : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings.

• Superior document: Lecture Notes in Computer Science Series ; v.12077
• Author: Goubault-Larrecq, Jean.
• TeilnehmendeR: König, Barbara.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2020.; ©2020.
• Year of Publication: 2020
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (657 pages)

Table of Contents

Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Neural Flocking: MPC-based Supervised Learning of Flocking Controllers -- 1 Introduction -- 2 Background -- 2.1 Model-Predictive Control -- 2.2 Declarative Flocking -- 3 Additional Control Objectives -- 4 Neural Flocking -- 4.1 Training Distributed Flocking Controllers -- 5 Experimental Evaluation -- 5.1 Preliminaries -- 5.2 Results for Basic Flocking -- 5.3 Results for Obstacle and Predator Avoidance -- 5.4 DNC Generalization Results -- 5.5 Statistical Model Checking Results -- 6 Related Work -- 7 Conclusions -- References -- On Well-Founded and Recursive Coalgebras -- 1 Introduction -- 2 Preliminaries -- 2.1 Algebras and Coalgebras. -- 2.2 Preservation Properties. -- 2.3 Factorizations. -- 2.4 Chains. -- 3 Recursive Coalgebras -- 4 The Next Time Operator and Well-Founded Coalgebras -- 5 The General Recursion Theorem and its Converse -- 6 Closure Properties of Well-founded Coalgebras -- 7 Conclusions -- References -- Timed Negotiations* -- 1 Introduction -- 2 Negotiations: Definitions and Brexit example -- 3 Timed Negotiations -- 4 High level view of the main results -- 5 Deterministic Negotiations -- 6 Sound Negotiations -- 7 k-Layered Negotiations -- 7.1 Algorithmic properties -- 7.2 Minimal Execution Time -- 8 Conclusion -- References -- Cartesian Difference Categories -- 1 Introduction -- 2 Cartesian Differential Categories -- 2.1 Cartesian Left Additive Categories -- 2.2 Cartesian Differential Categories -- 3 Change Action Models -- 3.1 Change Actions -- 3.2 Change Action Models -- 4 Cartesian Difference Categories -- 4.1 Infinitesimal Extensions in Left Additive Categories -- 4.2 Cartesian Difference Categories -- 4.3 Another look at Cartesian Differential Categories -- 4.4 Cartesian Difference Categories as Change Action Models -- 4.5 Linear Maps and ε-Linear Maps.

5 Examples of Cartesian Difference Categories -- 5.1 Smooth Functions -- 5.2 Calculus of Finite Diffferences -- 5.3 Module Morphisms -- 5.4 Stream calculus -- 6 Tangent Bundles in Cartesian Di erence Categories -- 6.1 The Tangent Bundle Monad -- 6.2 The Kleisli Category of T -- 7 Conclusions and Future Work -- References -- Contextual Equivalence for Signal Flow Graphs -- 1 Introduction -- 2 Background: the Affine Signal Flow Calculus -- 2.1 Syntax -- 2.2 String Diagrams -- 2.3 Denotational Semantics and Axiomatisation -- 2.4 Affine vs Linear Circuits -- 3 Operational Semantics for Affine Circuits -- 3.1 Trajectories -- 4 Contextual Equivalence and Full Abstraction -- 4.1 From Polynomial Fractions to Trajectories -- 4.2 Proof of Full Abstraction -- 5 Functional Behaviour and Signal Flow Graphs -- 6 Realisability -- 7 Conclusion and Future Work -- References -- Parameterized Synthesis for Fragments of First-Order Logic over Data Words -- 1 Introduction -- 2 Preliminaries -- 3 Parameterized Synthesis Problem -- 4 FO[˘] and Parameterized Vector Games -- 4.1 Satisfiability and Normal Form for FO[˘] -- 4.2 From Synthesis to Parameterized Vector Games -- 5 Results for FO[˘] via Parameterized Vector Games -- 6 Conclusion -- References -- Controlling a random population -- 1 Introduction -- 2 The stochastic control problem -- 3 The sequential ow problem -- 4 Reduction of the stochastic control problem to the sequential flow problem -- 5 Computability of the sequential ow problem -- 6 Conclusions -- Acknowledgements -- References -- Decomposing Probabilistic Lambda-Calculi -- 1 Introduction -- 1.1 Related Work -- 2 The Probabilistic Event λ-Calculus ^PE -- 3 Properties of Permutative Reduction -- 4 Confluence -- 4.1 Parallel Reduction and Permutative Reduction -- 4.2 Complete Reduction -- 5 Strong Normalization for Simply-Typed Terms.

6 Projective Reduction -- 7 Call-by-value Interpretation -- 8 Conclusions and Future Work -- Acknowledgments -- References -- On the k-synchronizability of Systems -- 1 Introduction -- 2 Preliminaries -- 3 k-synchronizable Systems -- 4 Decidability of Reachability for k-synchronizable Systems -- 5 Decidability of k-synchronizability for Mailbox Systems -- 6 k-synchronizability for Peer-to-Peer Systems -- 7 Concluding Remarks and Related works -- References -- General Supervised Learning as Change Propagation with Delta Lenses -- 1 Introduction -- 2 Background: Update propagation and delta lenses -- 2.1 Why deltas. -- 2.2 Consistency restoration via update propagation: An Example -- 2.3 Update propagation and update policies -- 2.4 Delta lenses -- 3 Asymmetric Learning Lenses with Amendments -- 3.1 Does Bx need categorical learning? -- 3.2 Ala-lenses -- 4 Compositionality of ala-lenses -- 4.1 Compositionality of update policies: An example -- 4.2 Sequential composition of ala-lenses -- 4.3 Parallel composition of ala-lenses -- 4.4 Symmetric monoidal structure over ala-lenses -- 4.5 Functoriality of learning in the delta lens setting -- 5 Related work -- 6 Conclusion -- A Appendices -- A.1 Category of parameterized functors pCat -- A.2 Ala-lenses as categorification of ML-learners -- References -- Non-idempotent intersection types in logical form -- Introduction -- 1 Notations and preliminary definitions -- 2 The relational model of the λ-calculus -- 3 The simply typed case -- 3.1 Why do we need another system? -- 3.2 Minimal LJ(I) -- 3.3 Basic properties of LJ(I) -- 3.4 Relation between intersection types and LJ(I) -- 4 The untyped Scott case -- 4.1 Formulas -- 5 Concluding remarks and acknowledgments -- References -- On Computability of Data Word Functions Defined by Transducers -- 1 Introduction -- 2 Data Words and Register Transducers.

2.1 Register Transducers -- 2.2 Technical Properties of Register Automata -- 3 Functionality, Equivalence and Composition of NRT -- 4 Computability and Continuity -- 5 Test-free Register Transducers -- References -- Minimal Coverability Tree Construction Made Complete and Efficient -- 1 Introduction -- 2 Covering abstractions -- 2.1 Petri nets: reachability and covering -- 2.2 Abstraction and acceleration -- 3 A coverability tree algorithm -- 3.1 Specification and illustration -- 3.2 Correctness Proof -- 4 Tool and benchmarks -- 5 Conclusion -- References -- Constructing Infinitary Quotient-Inductive Types -- 1 Introduction -- 2 QW-types -- 3 Quotient-inductive types -- 3.1 General QIT schemas -- 4 Construction of QW-types -- 5 Conclusion -- References -- Relative full completeness for bicategorical cartesian closed structure -- 1 Introduction -- 2 Cartesian closed bicategories -- 2.1 Bicategories -- 2.2 fp-Bicategories -- 2.3 Cartesian closed bicategories -- 3 Bicategorical glueing -- 4 Cartesian closed structure on the glueing bicategory -- 4.1 Finite products in gl(J) -- 4.2 Exponentials in gl(J) -- 5 Relative full completeness -- References -- A duality theoretic view on limits of finite structures -- 1 Introduction -- 2 Preliminaries -- 2.1 Stone-Priestley duality -- 2.2 Stone duality and logic: type spaces -- 2.3 Duality and logic on words -- 3 The space г -- 3.1 The algebraic structure on г -- 3.2 The retraction г → [0, 1] -- 4 Spaces of measures valued in г and in [0, 1] -- 5 The г-valued Stone pairing and limits of finite structures -- 5.1 The г-valued Stone pairing and logic on words -- 5.2 Limits in the spaces of measures -- 6 The logic of measures -- Conclusion -- References -- Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing -- 1 Introduction -- 2 A simple forward-mode AD translation.

3 Semantics of differentiation -- 4 Extending the language: variant and inductive types -- 5 Categorical analysis of forward AD and its correctness -- 6 A continuation-based AD algorithm -- 7 Discussion and future work -- References -- Deep Induction: Induction Rules for (Truly) Nested Types* -- 1 Introduction -- 2 The Key Idea -- 3 Extending to Nested Types -- 4 Theoretical Foundations -- 4.1 Categorical Preliminaries -- 4.2 Syntax and Semantics of ADTs -- 4.3 Induction Rules for ADTs -- 4.4 Syntax and Semantics of Nested Types -- 5 The General Methodology -- 6 Related Work and Directions for Further Investigation -- References -- Exponential Automatic Amortized Resource Analysis* -- 1 Introduction -- 2 Language and Cost Semantics -- 3 Automatic Amortized Resource Analysis -- 4 Exponential Potential -- 5 Mixed Potential -- 6 Exponentials, Polynomials, and Logarithms -- 7 Conclusion and Future Work -- References -- Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness -- 1 Introduction -- 2 Preliminaries -- 3 Pomset contexts -- 4 Concurrent Kleene Algebra with Hypotheses -- 4.1 Reification -- 4.2 Factoring the exchange law -- 4.3 Lifting -- 5 Instantiation to CKA with Observations -- 6 Discussion -- References -- Graded Algebraic Theories -- 1 Introduction -- 2 Preliminaries -- 2.1 Enriched Category Theory -- 2.2 Graded Monads -- 2.3 Day Convolution -- 2.4 Categories Enriched in a Presheaf Category -- 3 Graded Algebraic Theories -- 3.1 Equational Logic -- 3.2 Free Models -- 3.3 Examples -- 4 Graded Lawvere Theories -- 5 Equivalence -- 5.1 Graded Algebraic Theories and Graded Lawvere Theories -- 5.2 Graded Lawvere theories and Finitary Graded Monads -- 6 Combining E ects -- 6.1 Sums -- 6.2 Tensor Products -- 7 Related Work -- 8 Conclusions and Future Work -- References.

A Curry-style Semantics of Interaction: From untyped to second-order lazy λμ-calculus.