Types.- Comprehensive parametric polymorphism:categorical models and type theory.- Guarded Dependent Type Theory withCoinductive Types.- Dependent Types and Fibred Computational Effects.- GameSemantics for Bounded Polymorphism.- Recursion and Fixed-Points Join InverseCategories as Models of Reversible Recursion.- A Coalgebraic View of BarRecursion and Bar Induction.- A New Foundation for Finitary Corecursion.-Fixed-point elimination in the Intuitionistic Propositional Calculus.- Verificationand Program Analysis. A Theory of Monitors.- Contextual approximation andhigher-order procedures.- A Theory of Slicing for Probabilistic Control Flow Graphs.-Verification of parameterized communicating automata via split-width.- Automata,Logic, Games - Robust Equilibria in Mean-Payoff Games.- Quantifier Alternationfor Infinite Words.-Synchronizing automata over nested words.- On Freeze LTLwith Ordered Attributes.- Regular transformations of data words through origininformation.- Probabilistic and Timed Systems - Trace Refinement in LabelledMarkov Decision Processes.- Qualitative Analysis of VASS-Induced MDPs.- MetricTemporal Logic with Counting.- Distributed Synthesis in Continuous Time.- ProofTheory and Lambda Calculus Unary Resolution: Characterizing Ptime.- Focused andSynthetic Nested Sequents.- Strong Normalizability as a Finiteness Structurevia the Taylor Expansion of lambda-terms.- Reasoning about call-by-need bymeans of types.- Algorithms for Infinite Systems Coverability Trees for PetriNets with Unordered Data.- Shortest paths in one-counter systems.- TheInvariance Problem for Matrix Semigroups.- Order-Sorted Rewriting andCongruence Closure.- Monads.- Towards a formal theory of graded monads.- ProfiniteMonads, Profinite Equations, and Reiterman's Theorem.

This book constitutes the proceedings of the 19thInternational Conference on Foundations of Software Science and ComputationStructures, FOSSACS 2016, which took place in Eindhoven, The Netherlands, inApril 2016, held as Part of the European Joint Conferences on Theory andPractice of Software, ETAPS 2016.

The 31 full papers presented in this volume werecarefully reviewed and selected from 85 submissions. They were organized intopical sections named: types; recursion and fixed-points; verification andprogram analysis; automata, logic, games; probabilistic and timed systems;proof theory and lambda calculus; algorithms for infinite systems; and monads.