Foundations of Software Science and Computation Structures: 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint ... Ireland, April 25–30, 2020, Proceedings

ETAPS Foreword
Preface
Organization
Contents
1  Neural Flocking: MPC-based SupervisedLearning 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
2 
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
3 
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
4  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
5 
Contextual Equivalence for Signal Flow Graphs
	1 Introduction
	2 Background: the Ane Signal Flow Calculus
		2.1 Syntax
		2.2 String Diagrams
		2.3 Denotational Semantics and Axiomatisation
		2.4 Ane 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
6 
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 Satisability and Normal Form for FO[∼]
		4.2 From Synthesis to Parameterized Vector Games
	5 Results for FO[∼]
 via Parameterized Vector Games
	6 Conclusion
	References
7 
Controlling a random population*
	1 Introduction
	2 The stochastic control problem
	3 The sequential flow
 problem
	4 Reduction of the stochastic control problem to thesequential flow problem
	5 Computability of the sequential flow problem
	6 Conclusions
	References
8 Decomposing Probabilistic Lambda-Calculi
	1 Introduction
		1.1 Related Work
	2 The Probabilistic Event λ-Calculus ΛPE
	3 Properties of Permutative Reduction
	4 Conuence
		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
	References
9 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
10 
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
	References
11 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
	5 Concluding remarks and acknowledgments
	References
12 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
13 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
14 
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
15 Relative full completeness for bicategorical cartesian closed structure
	1 Introduction
	2 Cartesian closed bicategories
		2.1 Bicategories
	3 Bicategorical glueing
	4 Cartesian closed structure on the glueing bicategory
		4.1 Finite products in gl(J)
	5 Relative full completeness
	References
16 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
	6 The logic of measures
	Conclusion
	References
17 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
18
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
		4.5 Induction Rules for Nested Types
	5 The General Methodology
	6 Related Work and Directions for Further Investigation
	References
19 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
20
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
21 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 Eects
		6.1 Sums
		6.2 Tensor Products
	7 Related Work
	8 Conclusions and Future Work
	References
22 A Curry-style Semantics of Interaction: From untyped to second-order lazy λµ-calculus
	1 Introduction
		1.1 Program Equivalence and Polymorphism
	2 Typed Labelled Transition Systems
		2.1 Parallel Composition with Hiding
	3 The Lazy λµ-calculus
		3.1 A Typing System
		3.2 A Typed Interaction Structure
	4 A Polymorphic Type System
		4.1 Second-Order Configuration Types
		4.2 A Second-Order Typed Interaction Structure
	5 Conclusions and Further Directions
	References
23 An Axiomatic Approach toReversible Computation⋆
	1 Introduction
	2 Labelled Transition Systems with Independence
	3 Basic Properties
	4 Causal Safety and Causal Liveness
		4.1 Events
		4.2 CS and CL via Independence of Transitions
		4.3 CS and CL via Ordering of Events
		4.4 CS and CL via Independent Events
		4.5 Polychotomy
	5 Coinitial Independence
	6 Case Studies
	7 Conclusion, Related and Future Work
	References
24 An Auxiliary Logic on Trees: on the Tower-hardness of logics featuring reachability and submodel reasoning
	1 Introduction
	2 The definition of an Auxiliary Logic on Trees
	3 On the complexity and expressive power of ALT
		3.1 Towards the TOWER-hardness of SAT(ALT): how to encode finite words.
		3.2 Inexpressibility results via the Ehrenfeucht-Fraïssé games for ALT
		3.3 PITL on marked words and the TOWER-hardness of SAT(ALT)
	4 Revisiting TOWER-hard logics with ALT
		4.1 From ALT to First-Order Separation Logic
		4.2 From ALT to Quantified Computation Tree Logic
		4.3 From ALT to Modal Logic of Heaps and Modal Separation Logic
	5 Conclusions
	References
25 The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
	1 Introduction
	2 Preliminaries
		2.1 Stubborn sets
		2.2 Weak and Stutter Equivalence
	3 Counter-Example
	4 Strengthening Condition D1
		4.1 Implementation
		4.2 Correctness
		4.3 Deterministic LSTSs
	5 Safe Logics
		5.1 Reachability properties
		5.2 Deterministic LSTSs and CTL_X Model Checking
	6 Petri Nets
	7 Related Work
	8 Conclusion
	References
26 Semantical Analysis of Contextual Types
	1 Introduction
	2 Presheaves for Higher-Order Abstract Syntax
	3 Internal Language
	4 From Presheaves to Contextual Types
		4.1 A Universe of Representables
		4.2 Higher-Order Abstract Syntax
		4.3 Closed Objects
		4.4 Contextual Objects
	5 Simple Contextual Modal Type Theory
		5.1 Interpretation
	6 Presheaves on a Small Category with Attributes
		6.1 Yoneda CwA
	7 Conclusion
	References
27 Ambiguity, Weakness, and Regularity in Probabilistic Büchi Automata
	1 Introduction
	2 Preliminaries
	3 Ambiguity of PBA
		3.1 From classical to probabilistic automata
		3.2 From probabilistic to classical automata
		3.3 Threshold Semantics
	4 Complexity results
	5 Weakness in Probabilistic Büchi Automata
	6 Conclusion
	References
28 Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store\'
	1 Introduction
	2 Preliminaries
	3 A Call-by-Value Language with Local References
	4 Full Ground Store in the Abstract
	5 Intermezzo: BI-Hyperdoctrines and BI-Algebras
	6 A Higher Order Logic for Full Ground Store
	7 Examples
	8 Conclusions and Further Work
	References
29 Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
	1 Introduction
	2 Syntax of QPL
	3 Operational Semantics of QPL
	4 W*-algebras
	5 Denotational Semantics of QPL
		5.1 Interpretation of Types
		5.2 Copying and Discarding
		5.3 Interpretation of Terms
		5.4 Interpretation of Configurations
		5.5 Soundness, Adequacy and Big-step Invariance
	6 Conclusion and Related Work
	References
30 
Spinal Atomic Lambda-Calculus
	1 Introduction
	2 Typing a λ-calculus in open deduction
		2.1 The Sharing Calculus
	3 The Spinal Atomic λ-Calculus
		3.1 Compilation and Readback.
		3.2 Rewrite Rules.
	4 Strong Normalisation of Sharing Reductions
	5 Preservation of Strong Normalisation and Conuence
	6 Conclusion, related work, and future directions
	References
31 Learning Weighted Automataover Principal Ideal Domains*
	1 Introduction
	2 Overview of the Approach
		2.1 Example: Learning a Weighted Language over the Reals
		2.2 Learning Weighted Languages over Arbitrary Semirings
	3 Preliminaries
	4 General Algorithm for WFAs
		4.1 Termination of the General Algorithm
	5 Issues with Arbitrary Semirings
	6 Learning WFAs over PIDs
	7 Discussion
	References
32 The Polynomial Complexity of Vector Addition Systems with States
	1 Introduction
		1.1 Overview and Illustration of Results
		1.2 Related Work
	2 Preliminaries
	3 A Dichotomy Result
	4 Main Algorithm
		4.1 Complexity of Algorithm 1
	5 Proof of the Upper Bound Theorem
	6 Proof of the Lower Bound Theorem
	7 The Size of the Exponents
	8 Exponential Witness
	References
Author Index