Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings

ETAPS Foreword......Page 6
Preface......Page 8
Organization......Page 9
Fundamental Algorithmic Problems and Challenges in Dynamical and Cyber-Physical Systems (Abstract of Invited Talk)......Page 12
Contents......Page 13
Coherence Spaces and Higher-Order Computation......Page 16
 1 Introduction......Page 17
  2.1 Uniform Spaces......Page 19
  2.2 Coherence Spaces......Page 21
  3.1 Coherence Spaces with Totality......Page 23
  3.2 Uniformities Induced by Co-Totality......Page 25
  4.1 Representations as a Realizability Model......Page 28
  4.2 Linear Realizability for Separable Metrizable Spaces......Page 29
 5 Related and Future Work......Page 31
 References......Page 32
 1 Introduction......Page 34
 2 The Model of Probabilistic Coherence Spaces......Page 37
  3.1 Lafont\'s Model......Page 40
  3.2 Melliès, Tasson and Tabareau\'s Formula......Page 41
 4 The Case of Probabilistic Coherence Spaces......Page 42
  4.1 The Approximants AN......Page 43
  4.2 The Limit A......Page 45
  4.3 The Free and Entire Exponential Modalities Are the Same......Page 48
 References......Page 49
 1 Introduction......Page 50
  1.1 Enriched Categories and Change of Base......Page 51
 2 Coherence Spaces and Weighted Relations......Page 52
 3 An Example: Games and History-Sensitive Strategies......Page 54
  3.1 Coherence Space Enrichment of Games......Page 55
 4 Additives and Exponentials......Page 57
  4.1 The Cofree Commutative Comonoid......Page 58
  4.2 Preservation of Cofree Commutative Comonoids......Page 60
 5 R-Weighted Idealized Algol......Page 61
  5.1 Denotational Semantics......Page 63
 6 Conclusions and Further Directions......Page 64
 References......Page 65
 1 Introduction......Page 67
 2 Main Result......Page 69
  3.1 (,,) as a Regular Tree Language......Page 71
  3.2 Irreducibility and Aperiodicity......Page 73
 4 Proof of the Main Theorem......Page 74
  4.1 Normalized Contexts......Page 75
  4.2 Decomposition......Page 76
  4.3 Explosive Context......Page 79
  4.4 Proof Sketch of Theorem1......Page 80
 6 Conclusion......Page 81
 References......Page 82
Algebra and Coalgebra......Page 83
 1 Introduction......Page 84
 2 Preliminaries......Page 86
 3 Coalgebraic Semantics of Polynomial odes......Page 88
 4 Algebraic Characterization of L-bisimilarity......Page 89
 5 Computing Invariants......Page 90
 7 Examples......Page 95
 8 Future and Related Work......Page 97
 References......Page 98
 1 Introduction......Page 101
 2 Relational Models of Failure......Page 105
 3 The Basic Algebraic Theory of Failure......Page 106
 4 A Stronger Theory of Failure......Page 112
 5 Related Work......Page 115
 6 Conclusion......Page 116
 References......Page 117
 1 Introduction......Page 119
 2 Preliminaries......Page 122
 3 Properties of the Companion......Page 124
 4 The Codensity Monad......Page 125
 5 Constructing the Companion by Codensity......Page 126
  5.1 Codensity and the Companion of a Monotone Function......Page 127
 6 Causality by Codensity......Page 128
  7.1 Solving Equations via Causal Algebras......Page 130
  7.2 Causal Algebras and Distributive Laws......Page 131
  7.3 Soundness of Up-to Techniques......Page 132
 8 Abstract GSOS......Page 133
 References......Page 134
 1 Introduction......Page 137
 2 Preliminaries......Page 140
 3 Strings and Languages with Name Binding......Page 141
 4 Regular Bar Expressions......Page 142
 5 Regular Nondeterministic Nominal Automata......Page 145
 6 Name-Dropping Register Automata......Page 149
 7 Deciding Inclusion under Global and Local Freshness......Page 151
 8 Conclusions......Page 152
 References......Page 153
Games and Automata......Page 156
 1 Introduction......Page 157
 2 Preliminaries......Page 160
 3 General Conditions for the Existence of Weak SPEs......Page 163
 4 First Application......Page 168
 5 Second Application......Page 170
 References......Page 172
 1 Introduction......Page 174
 2 Weighted Games......Page 176
 3 Solving Divergent Weighted Games......Page 177
 4 Weighted Timed Games......Page 182
 5 Solving Divergent Weighted Timed Games......Page 184
 References......Page 189
 1 Introduction......Page 191
 2 Preliminaries......Page 195
 3 Equivalence with an Infinite-State Mean-Payoff Game......Page 197
  5.1 Analyzing Winning Plays......Page 199
  5.2 Strategies Described by Finite Trees......Page 200
  5.3 Analyzing Winning Strategies......Page 202
 6 Multi-dimensional Average-Energy Games......Page 204
 References......Page 206
 1 Introduction......Page 208
 2 Preliminaries......Page 211
 3 Logic of Repeating Values on Data Trees......Page 212
  4.1 Branching VASS......Page 213
  4.2 Merging VASS......Page 214
  4.3 Decision Problems......Page 215
 5 Satisfiability of LRVD on data trees......Page 216
 6 Obtaining Equivalence with VASSk......Page 219
 7 From LRV to MVASSk......Page 221
 8 Discussion......Page 222
 References......Page 223
Automata, Logic and Formal Languages......Page 225
 1 Introduction......Page 226
 2 Definitions and Examples......Page 229
 3 Lipschitz and Branching Twinning Properties......Page 232
  3.2 Branching Twinning Property of Order k......Page 233
  3.3 Equivalence of Lipschitz and Branching Twinning Properties......Page 234
 4 Constructing a k-sequential Weighted Automaton......Page 235
 5 Cost Register Automata with Independent Registers......Page 236
 6 The Case of Transducers......Page 238
 7 Decidability of BTPk and Computation of the Sequentiality Degree......Page 239
 References......Page 240
 1 Introduction......Page 242
 2 Preliminaries......Page 245
 3 Hierarchical Probabilistic Automata......Page 247
  3.1 Regularity of HPAs with Isolated Cut-points......Page 248
 4 Emptiness Under Isolation......Page 249
 5 On the Value Decision Problem......Page 252
  5.1 Computing the Value of 1-HPAs......Page 254
 6 Conclusions......Page 256
 References......Page 257
 1 Introduction......Page 259
 2 Preliminaries......Page 260
 3 -Regular Expressions......Page 261
 4 Partial Derivatives......Page 263
 5 Nullability......Page 264
 6 Derivation......Page 265
 7 Correctness......Page 268
 8 Finiteness......Page 270
 9 Automaton Construction......Page 272
 References......Page 274
 1 Introduction......Page 276
  2.2 Dynamic Complexity......Page 278
  2.4 Main Result......Page 280
 3 One-Letter (Undirected) Dyck Reachability Problems......Page 281
 4 n-letter Dyck Reachability Problem......Page 282
  4.1 From the Near-Dyck Reachability Problem to the Dyck Reachability Problem......Page 283
  4.2 From the Alternating Reachability Problem to the Near-Dyck Reachability Problem......Page 284
 5 n-letter Undirected Dyck Reachability Problem......Page 286
 References......Page 290
Proof Theory......Page 292
 1 Introduction......Page 293
 2 Proof by Infinite Descent......Page 295
 3 -proofs......Page 297
 4 Cyclic Arithmetic......Page 301
 5 Conservativity of CA over PA......Page 303
 6 Büchi Automata in ACA0......Page 306
 References......Page 308
 1 Introduction......Page 311
 2 Brotherston-Simpson Conjecture......Page 312
  2.2 Cyclic Proof System  CLKID......Page 313
  3.1 Hydra Problem......Page 314
  3.2 2-Hydra Statement......Page 315
  3.3 2-Hydra Statement in Cyclic-Proof System......Page 316
  4.2 Definition of the Structure M......Page 317
  4.3 The Measure of the Subsets of M  Closed Under 0 and  s......Page 318
  5.1 The Set  D  of Subsets of M......Page 319
  5.2 The Family  R  of Partial Bijections on M......Page 320
 6 A Quantifier Elimination Result for Partial Bijections......Page 321
  6.1 A Notion of Normal Form for the Language  R......Page 323
  6.2 A Quantifier Elimination Result for  R......Page 324
 8 Non-conservativity of Martin-Löf\'s Inductive Definition System......Page 325
 References......Page 326
Probability......Page 328
 1 Introduction......Page 329
  2.1 Labelled Markov Chains......Page 332
  2.2 Exact and Approximate Probabilistic Bisimulations......Page 333
 3 Approximate Probabilistic Trace Equivalence for LMCs......Page 334
  3.1 Interpretation and Application of -Trace Equivalence......Page 335
 4 -Probabilistic Bisimulation Induces Approximate Probabilistic Trace Equivalence......Page 336
 5 Application to Model Checking of Continuous-State LMCs......Page 339
 6 Case Study......Page 340
 7 Other Notions of -Bisimulation......Page 342
 References......Page 343
 1 Introduction......Page 346
  2.1 Stochastic String Rewriting and Word Occurrences......Page 350
  3.1 Transition Functions and q-Matrices......Page 351
  3.2 The Abstract Cauchy Problem for Ptf......Page 352
  3.3 Banach Space Wanted!......Page 353
  4.1 Weighted C0-Spaces and Drift Functions......Page 354
  4.3 On the Domain of the Generator......Page 355
  4.4 Applications: String Rewriting and Petri Nets......Page 356
 5 Computability......Page 357
 6 The Finite Dimensional Case and PTIME via ODEs......Page 358
 7 Conclusion......Page 360
 References......Page 361
 1 Introduction......Page 363
 2 Preliminaries......Page 365
  3.2 Bayesian Inversion in the Finite Subcategory of Krn......Page 366
  3.3 Bayesian Inversion in Krn......Page 367
  3.4 Pointfulness Is Harmful......Page 368
  4.1 The Category Ban......Page 369
  4.2 Duality in Banach Cones......Page 371
 5 Pointless Bayesian Inversion......Page 372
  5.1 Representing Krn Arrows as AMKs......Page 373
  5.2 Bayesian Inversion in Krn......Page 374
 6 Pointless Bayesian Inversion Through Couplings......Page 375
 References......Page 376
 1 Introduction......Page 378
 2 Probabilistic Choice Operators, Informally......Page 380
 3 The Full Calculus T,R,X......Page 381
  3.1 Operational Semantics......Page 382
  3.2 Almost-Sure Termination......Page 383
  3.3 On Fragments of T,R,X: A Roadmap......Page 386
 4 Binary Probabilistic Choice......Page 388
 5 Countable Probabilistic Choice......Page 389
 7 Conclusions......Page 392
 References......Page 393
Concurrency......Page 395
 1 Introduction......Page 396
 2 Simply-Typed Asynchronous -Calculus......Page 398
  3.1 Arenas......Page 399
  3.2 DAG-based Plays......Page 400
  3.3 Strategies and Composition......Page 402
  3.4 Distributive-Closed Freyd Category......Page 404
  3.5 Relation to Sequential Game Models......Page 406
 4 Game Semantics of the -calculus......Page 407
 5 Discussion: Relationally-Describable Process......Page 408
 6 Related Work......Page 409
 7 Conclusion and Future Work......Page 410
 References......Page 411
 1 Introduction......Page 414
 2 Event Structures and Regularity......Page 416
  3.1 Syntax......Page 418
  3.2 Semantics......Page 420
  4.1 Constants and Definition Lists......Page 421
  4.3 The Stop Condition......Page 423
  4.4 Model Checking a Formula Through Tableaux......Page 425
 5 Conclusions......Page 427
 References......Page 429
 1 Introduction......Page 431
  1.1 Contributions......Page 432
 2 Related Work......Page 433
 3 Core Choreographies and Stateful Processes......Page 434
 4 Extraction from SP......Page 437
 5 Asynchrony......Page 442
 6 Extensions and Applications......Page 445
 References......Page 446
 1 Introduction......Page 448
  2.1 CFSMs and Their Properties......Page 450
 3 A Compatibility Relation for CFSMs......Page 452
 4 Undecidability of the   `39`42`\"613A``45`47`\"603A-relation......Page 455
  4.1 Decidable Sub-classes of CFSMs......Page 458
 5 Correspondence Between Compatibility and Subtyping......Page 459
 6 Conclusions and Related Work......Page 462
 References......Page 463
Lambda Calculus and Constructive Proof......Page 465
 1 Introduction......Page 466
 2 Extension Orders......Page 469
 3 Term Orders......Page 470
  3.2 The Applicative RPO......Page 471
  3.3 A Graceful Higher-Order RPO......Page 472
  3.4 An Optimized Variant of the Graceful Higher-Order RPO......Page 473
 4 Properties......Page 474
 5 Examples......Page 478
 6 Discussion......Page 481
 References......Page 482
 1 Introduction......Page 485
 2 Notations and Definitions......Page 486
 3 State of the Art: Two Constructive Fragments of Predicate Logic......Page 488
 4 The Weakening Normalization......Page 490
 5 A New Constructive Fragment......Page 493
 6 The Full Constructivization Algorithm......Page 494
 References......Page 499
Semantics and Category Theory......Page 501
 1 Introduction......Page 502
 2 A Light Modality for Typed Lambda Calculus......Page 503
 3 Denotational Semantics......Page 507
  4.1 Meta-Types......Page 509
  4.2 Constraint Typing Rules......Page 510
  4.3 Unification Algorithm......Page 511
  4.4 Generation of Guard Constraints......Page 514
  4.5 Type Inference Algorithm......Page 515
 6 Conclusions and Future Work......Page 517
 References......Page 518
 1 Introduction......Page 520
 2 Preliminaries......Page 522
 3 Guarded Monads......Page 523
 4 Parametrizing Guardedness......Page 526
 5 Complete Elgot Monads and Iteration Congruences......Page 528
 6 A Sandwich Theorem for Elgot Monads......Page 533
 8 Conclusions and Further Work......Page 534
 References......Page 535
 1 Introduction......Page 537
 2 Background: Type Theory with Quotient Inductive-Inductive Types......Page 540
  3.1 The Definition and Its Elimination Principles......Page 541
  3.2 -Complete Partial Orders......Page 543
  3.3 A Characterisation of the Relation......Page 544
  4.1 The Delay Monad and Monotone Sequences......Page 546
  4.2 Monotone Sequences and the QIIT Construction......Page 547
  5.1 Nonterminating Functions as Fixed Points......Page 549
  5.2 Functions from the Reals......Page 550
 References......Page 551
  1.1 Intensionality as a Logical Construct......Page 553
  1.2 Prospectus......Page 554
 2 Modality-as-Intension......Page 555
 3 Exposures......Page 556
  3.1 Cartesian Exposures......Page 557
  3.2 Evaluators, Quotation Devices, and Comonadic Exposures......Page 558
 5 Consistency, Truth and Provability: Gödel and Tarski......Page 559
 6 An Exposure on Arithmetic......Page 561
 7 Where Do IFPs Come From?......Page 562
 8 The Recursion Theorems......Page 563
 9 An Exposure on Assemblies......Page 564
  9.1 Passing to a P-category......Page 565
 10 Rice\'s Theorem......Page 566
 11 Conclusion......Page 567
 References......Page 568
Author Index......Page 570