Foundations of software science and computation structures : 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016 : proceedi

This book constitutes the proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016, which took place in Eindhoven, The Netherlands, in April 2016, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016. The 31 full papers presented in this volume were carefully reviewed and selected from 85 submissions. They were organized in topical sections named: types; recursion and fixed-points; verification and program analysis; automata, logic, games; probabilistic and timed systems; proof theory and lambda calculus; algorithms for infinite systems; and monads. Front Matter....Pages I-XI Front Matter....Pages 1-1 Comprehensive Parametric Polymorphism: Categorical Models and Type Theory....Pages 3-19 Guarded Dependent Type Theory with Coinductive Types....Pages 20-35 Dependent Types and Fibred Computational Effects....Pages 36-54 Game Semantics for Bounded Polymorphism....Pages 55-70 Front Matter....Pages 71-71 Join Inverse Categories as Models of Reversible Recursion....Pages 73-90 A Coalgebraic View of Bar Recursion and Bar Induction....Pages 91-106 A New Foundation for Finitary Corecursion....Pages 107-125 Fixed-Point Elimination in the Intuitionistic Propositional Calculus....Pages 126-141 Front Matter....Pages 143-143 A Theory of Monitors....Pages 145-161 Contextual Approximation and Higher-Order Procedures....Pages 162-179 A Theory of Slicing for Probabilistic Control Flow Graphs....Pages 180-196 Verification of Parameterized Communicating Automata via Split-Width....Pages 197-213 Front Matter....Pages 215-215 Robust Equilibria in Mean-Payoff Games....Pages 217-233 Quantifier Alternation for Infinite Words....Pages 234-251 Synchronizing Automata over Nested Words....Pages 252-268 On Freeze LTL with Ordered Attributes....Pages 269-284 Regular Transformations of Data Words Through Origin Information....Pages 285-300 Front Matter....Pages 301-301 Trace Refinement in Labelled Markov Decision Processes....Pages 303-318 Qualitative Analysis of VASS-Induced MDPs....Pages 319-334 Metric Temporal Logic with Counting....Pages 335-352 Front Matter....Pages 301-301 Distributed Synthesis in Continuous Time....Pages 353-369 Front Matter....Pages 371-371 Focused and Synthetic Nested Sequents....Pages 373-389 Reasoning About Call-by-need by Means of Types....Pages 390-407 Front Matter....Pages 408-423 Coverability Trees for Petri Nets with Unordered Data....Pages 424-441 Shortest Paths in One-Counter Systems....Pages 443-443 The Invariance Problem for Matrix Semigroups....Pages 445-461 Order-Sorted Rewriting and Congruence Closure....Pages 462-478 Front Matter....Pages 479-492 Towards a Formal Theory of Graded Monads....Pages 493-509 Profinite Monads, Profinite Equations, and Reiterman’s Theorem....Pages 511-511 Back Matter....Pages 513-530 ....Pages 531-547