Foundations of Software Science and Computation Structures, 19 conf., FOSSACS 2016

• Publisher: Springer
• Year: 2016
• Tongue: English
• Leaves: 548
• Series: Springer Lecture notes in computer science 9634
• Category: Library

✦ Table of Contents

ETAPS Foreword......Page 6
Preface......Page 8
Organization......Page 9
Contents......Page 10
Types......Page 13
1 Introduction......Page 14
2 Comprehensive 2 Fibrations......Page 16
3 Comprehensive 2 Parametricity Graphs......Page 19
4 A Type System for Relational Reasoning......Page 21
5 Direct-Image and Pseudograph Relations......Page 25
6 Consequences of Parametricity......Page 26
7 Related and Further Work......Page 28
References......Page 29
1 Introduction......Page 31
2 Guarded Dependent Type Theory......Page 33
2.1 Fixed Points and Guarded Recursive Types......Page 35
2.2 Identity Types......Page 36
3 Examples......Page 37
4 Coinductive Types......Page 39
5 Example Programs with Coinductive Types......Page 41
6 Soundness......Page 43
7 Related Work......Page 44
References......Page 45
1 Introduction......Page 47
2 A Dependently-typed Effectful Language......Page 49
3.1 Fibred Category Theory Preliminaries......Page 52
3.2 Interpretation of Our Language in Fibred Adjunction Models......Page 54
3.3 Fibred Adjunction Models Based on the Families Fibration......Page 57
4.1 Algebraic Effects in the Syntax......Page 58
4.2 Algebraic Effects in the Semantics......Page 59
5.2 Domain-Theoretic Semantics for Recursion......Page 60
6 Conclusions and Future Work......Page 62
References......Page 63
1 Introduction......Page 66
2 Second Order Game Semantics......Page 67
2.1 Examples......Page 68
2.2 Legal Sequences and Strategies......Page 69
2.3 Instantiation......Page 70
3 Generic Strategies as Dinatural Transformations......Page 71
4 Semantics of Bounded Quantification......Page 72
5 A Stateful Language with Bounded Quantification......Page 74
5.1 Denotational Semantics......Page 76
5.2 Semantics of Terms......Page 77
6 Full Abstraction......Page 79
7 Further Directions......Page 80
References......Page 81
Recursion and Fixed-Points......Page 82
1 Introduction......Page 83
2 Background......Page 84
2.1 Joins and Compatibility......Page 87
2.2 Categories of Partial Maps......Page 88
3 As CPO-categories......Page 89
3.1 Reversible Fixed Points of Morphism Schemes......Page 90
3.2 Algebraic -compactness for Free!......Page 92
4 As Unique Decomposition Categories......Page 94
5 Conclusion......Page 97
References......Page 98
1 Introduction......Page 101
2 Bar Recursion......Page 103
3 Continuous Functions on Streams......Page 105
3.1 Individual Tabulations......Page 108
3.2 Global Tabulation......Page 109
4 Bar Induction......Page 111
References......Page 115
1 Introduction......Page 117
2 Preliminaries and Notation......Page 119
3 The Locally Finite Fixpoint......Page 120
4 Instances of the Locally Finite Fixpoint......Page 124
4.1 Generalized Powerset Construction......Page 125
4.2 The Languages of Non-deterministic Automata......Page 126
4.3 The Behaviour of Stack Machines......Page 127
4.4 Context-Free Languages and Constructively S-Algebraic Power Series......Page 128
4.5 Courcelle's Algebraic Trees......Page 130
5 Conclusions and Future Work......Page 132
References......Page 133
1 Introduction......Page 136
2 Notation and Elementary Concepts......Page 138
3 The Intuitionistic Propositional -Calculus......Page 139
4 Strong Monotone Functions and Fixed-Points......Page 141
5 A Digression on Fixpoints and Bisimulation Quantifiers......Page 143
6 The Elimination Procedure......Page 144
6.1 Strongly positive Elimination......Page 145
6.2 Weakly Negative Elimination......Page 147
7 Upper Bounds on Closure Ordinals......Page 148
References......Page 150
Verification and Program Analysis......Page 152
1 Introduction......Page 153
2 The Language......Page 155
3 Monitor Instrumentation......Page 156
4 Monitor Preorders......Page 159
5 Characterisation......Page 163
6 Conclusion......Page 166
References......Page 167
1 Introduction......Page 170
2 Idealized Algol......Page 172
3 Games......Page 173
4 Upper Bounds......Page 176
5 Lower Bounds......Page 182
6 Conclusion......Page 185
References......Page 186
1 Introduction......Page 188
2 Motivating Examples......Page 189
3 Control Flow Graphs......Page 191
4.1 Stores and Distributions......Page 193
4.3 One-Step Reduction......Page 194
4.4 Multi-step Reduction and Loops......Page 195
5 Conditions for Slicing......Page 196
7 Computing the (Least) Slice......Page 199
8 Extensions and Future Work......Page 202
9 Conclusion and Related Work......Page 203
References......Page 204
1 Introduction......Page 205
2 Parameterized Communicating Automata......Page 208
3 Split-Width......Page 211
4 Classes of Bounded Split-Width......Page 214
5 Tree Interpretation......Page 216
6 Further Results......Page 219
References......Page 220
Automata, Logic, Games......Page 222
1 Introduction......Page 223
2.1 Weighted Concurrent Games......Page 226
2.2 Equilibria Notions......Page 228
3 Stationary Strategies......Page 229
4.1 Deviator Game......Page 231
5.1 Multidimensional Objectives......Page 233
5.2 Correctness of the Objectives for Robustness......Page 234
6 Fixed Coalition Game......Page 235
7 Hardness......Page 237
References......Page 238
Quantifier Alternation for Infinite Words......Page 240
1.1 The Quantifier Alternation Hierarchy of First-Order Logic......Page 242
1.2 Decision Problems......Page 243
2.1 Semigroups and Wilke Algebras......Page 245
2.2 Logical Preorders......Page 247
3 Chains for Omega-Languages......Page 248
3.1 i-Chains and Separation for i......Page 250
4 A Separation Algorithm for Sigma2......Page 251
5 A Membership Algorithm for B-Sigma2......Page 253
6 A Separation Algorithm for 3......Page 254
7 Conclusion......Page 255
References......Page 256
1 Introduction......Page 258
2 Nested Words and Nested Word Automata......Page 261
3 Synchronizing Words for NWA......Page 262
4.1 Binary Tree Representation of Nested Words......Page 265
4.2 From Nested Word Automata to Tree Automata......Page 266
4.3 Pebble Games and Strahler Numbers......Page 267
4.4 Bounded Nonemptiness for Implicitly Presented Tree Automata......Page 269
5.1 Small-Cost Synchronizing Words in DFA......Page 270
5.2 Reduction to Short Synchronizing Nested Word......Page 271
References......Page 273
1 Introduction......Page 275
2 Semantics and Undecidability of LTL"3223379 qo......Page 279
3 Nested Counter Systems......Page 281
4 From LTL"3223379 tqo to NCS and Back......Page 285
5 Conclusion......Page 288
References......Page 289
1 Introduction......Page 291
2.1 Words, Strings and Data Words......Page 293
2.3 Transduction of Data Words......Page 294
2.5 Properties......Page 295
2.6 MSO k-types......Page 296
3 Two-Way Transducers on Data Words......Page 297
4.1 Streaming String Transducers with Data Variables and Parameters......Page 300
4.2 From Two-Way to One-Way Transducers......Page 302
4.3 From One-Way Transducers to MSO......Page 304
References......Page 306
Probabilistic and Timed Systems......Page 307
1 Introduction......Page 308
2.1 Labelled Markov Decision Processes......Page 310
3 Undecidability Results......Page 312
4.1 Pure Memoryless Strategies......Page 315
4.2 Memoryless Strategies......Page 317
5 Bisimulation......Page 319
References......Page 322
1 Introduction......Page 324
2.1 Markov Decision Processes......Page 326
2.2 VASS-MDPs......Page 327
2.3 Verification Problems for VASS-MDPs......Page 328
2.4 Undecidability in the General Case......Page 329
2.5 Model-Checking -calculus on Single-Sided VASS......Page 330
3.1 Undecidability in Presence of Deadlocks......Page 331
3.2 Sure (repeated) Reachability in Deadlock-Free P-VASS-MDPs......Page 332
3.3 Almost-Sure and Limit-Sure Reachability in Deadlock-Free P-VASS-MDPs......Page 333
4.2 Almost-Sure Problems in 1-VASS-MDPs......Page 334
4.3 Limit-Sure Reachability in 1-VASS-MDP......Page 336
5 Conclusion and Future Work......Page 338
References......Page 339
1 Introduction......Page 340
2 A Zoo of Timed Temporal Logics......Page 342
3.1 CTMTL Games......Page 344
4 Satisfiability Checking of Counting Logics......Page 350
5 Discussion and Related Work......Page 355
References......Page 356
1 Introduction......Page 358
2 Distributed Interactive Markov Chains......Page 361
2.1 Schedulers and Strategies......Page 362
2.2 Probability of Plays......Page 363
3 Schedulers Are Not that Powerful......Page 364
4 Undecidability Results......Page 365
4.2 Reduction from DEC-POMDP......Page 366
4.3 Undecidability of Qualitative Existence in DEC-POMDP......Page 367
5 Decidability for Non-urgent Models......Page 369
6 Discussion and Conclusion......Page 372
References......Page 373
Proof Theory and Lambda Calculus......Page 375
1 Introduction......Page 376
2.1 Flows and Wirings......Page 378
2.2 Representation of Words and Programs......Page 381
2.3 The Stack Semiring......Page 382
3 Pushdown Automata and PTIME Completeness......Page 384
4 Nilpotency in Stack and PTIME Soundness......Page 387
5 Unary Logic Programming......Page 388
6 Perspectives......Page 390
References......Page 391
1 Introduction......Page 393
2 Modal Logics and the Nested Sequent Calculus KN......Page 395
3 The Focused Systems KNwF and KNF......Page 397
3.1 Cut Elimination......Page 400
3.2 Completeness......Page 402
4 The Synthetic System......Page 404
4.1 Synthetic Substructures......Page 405
4.2 Cut Elimination......Page 406
5 Perspectives......Page 408
References......Page 409
1 Introduction......Page 411
2.1 Non-deterministic -calculus......Page 413
2.2 Resource Calculus and Taylor Expansion......Page 414
2.3 Finiteness Structures Induced by Antireduction......Page 417
3 Strongly Normalizing Terms Are D+ Typable......Page 419
4 D+ Typable Terms Are Finitary......Page 420
5 Finitary Terms Are Strongly Normalizing......Page 423
References......Page 425
A Appendix......Page 427
2 Call-by-name and Call-by-need......Page 429
3 Non-idempotent Intersection Types......Page 432
4 Characterization of name-normalizing Terms......Page 434
5 Characterization of need-normalizing Terms......Page 435
6 Soundness and Completeness......Page 439
7 Conclusion......Page 440
References......Page 442
Algorithms for Infinite Systems......Page 445
1 Introduction......Page 446
2 Model......Page 448
3 Simple Ideals......Page 452
4.1 Accelerations......Page 455
4.2 Coverability Trees......Page 456
5 Complexity Bounds......Page 457
5.1 Fast-Growing Complexity......Page 458
5.2 Upper Bounds......Page 459
6 Concluding Remarks......Page 460
References......Page 461
1 Introduction......Page 463
2 Summary......Page 465
3 Challenges and Techniques......Page 467
4 Preliminaries......Page 468
5.1 Proof Overview and Notation......Page 470
5.2 Normal Paths......Page 471
5.3 Length of Shortest Paths......Page 475
References......Page 478
1 Introduction......Page 480
1.1 Attacking the Invariance Problem......Page 481
2.1 Setting......Page 483
3.1 Finiteness of the Set of Essential Words......Page 486
3.2 Decidability of the Invariance Problem......Page 488
4.2 Locations......Page 489
5.1 Summary......Page 490
5.3 Future Work......Page 491
References......Page 492
1 Introduction......Page 494
2 Preliminaries on Order-Sorted Algebra......Page 497
3 Order-Sorted Rewriting and Equality......Page 500
3.1 Kind-Complete OS-Rewriting and Equational Deduction......Page 501
3.2 Conservativity Results......Page 504
4.1 Abstract Congruence Closure......Page 505
4.2 Deciding OS (,)-QF-Satisfiability......Page 506
5 Order-Sorted (,AC)-QF-Satisfiability......Page 507
6 Related Work and Conclusions......Page 508
References......Page 509
Monads......Page 511
1 Introduction......Page 512
2 Parametric Monads Are Graded Monads......Page 516
3 Adjunction Pairs Induced from Graded Monads......Page 517
3.1 The Eilenberg-Moore Construction......Page 518
3.2 The Kleisli Construction......Page 519
3.3 Resolutions of Graded Monads......Page 520
4.1 A 2-Category for Eilenberg-Moore Objects......Page 521
4.2 A 2-Category for Kleisli Objects......Page 523
5 Illustration: The Graded State Monad......Page 525
References......Page 528
1 Introduction......Page 530
2 Preliminaries......Page 532
3 Profinite Monads......Page 536
4.1 Pseudovarieties and Profinite (In-)equations......Page 538
4.2 Reiterman's Theorem for T-algebras......Page 539
5 Applications and Examples......Page 542
6 Conclusions and Future Work......Page 544
References......Page 545
Author Index......Page 547