Foundations of Software Science and Computation Structures : 18th International Conference, FOSSACS 2015, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings

This Book Constitutes The Proceedings Of The 18th International Conference On Foundations Of Software Science And Computation Structures, Fossacs 2015, Held In London, Uk, In April 2015, As Part Of The European Joint Conferences On Theory And Practice Of Software, Etaps 2015. The 28 Full Papers Presented In This Volume Were Carefully Reviewed And Selected From 93 Submissions. They Are Organized In Topical Sections Named: Semantics Of Programming Languages; Categorical Models And Logics; Concurrent, Probabilistic And Timed Systems; Automata, Games, Verification; Logical Aspects Of Computational Complexity; And Type Theory, Proof Theory And Implicit Computational Complexity. The Book Also Contains One Full Paper Invited Talk. Invited Talk -- Polarized Substructural Session Types -- Semantics Of Programming Languages I -- Synthesis Of Strategies And The Hoare Logic Of Angelic Nondeterminism -- An Infinitary Model Of Linear Logic -- Game Semantics And Normalization By Evaluation -- Foundations Of Differential Dataflow -- Categorical Models And Logics -- States Of Convex Sets -- A Categorical Semantics For Linear Logical Frameworks -- A Completeness Result For Finite λ-bisimulations -- Sequent Calculus In The Topos Of Trees -- Modal And Temporal Logics -- Coalgebraic Trace Semantics Via Forgetful Logics -- Unifying Hyper And Epistemic Temporal Logics -- Concurrent, Probabilistic And Timed Systems On The Total Variation Distance Of Semi-markov Chains -- Decidable And Expressive Classes Of Probabilistic Automata -- Knowledge = Observation + Memory + Computation -- Compositional Metric Reasoning With Probabilistic Process Calculi -- Semantics Of Programming Languages Ii -- Fragments Of Ml Decidable By Nested Data Class Memory Automata -- Operational Nominal Game Semantics -- Step-indexed Logical Relations For Probability -- Automata, Games, Verification -- Minimisation Of Multiplicity Tree Automata -- Robust Multidimensional Mean-payoff Games Are Undecidable -- The Cyclic-routing Uav Problem Is Pspace-complete -- Typing Weak Msol Properties -- Logical Aspects Of Computational Complexity Three Variables Suffice For Real-time Logic -- On Presburger Arithmetic Extended With Modulo Counting Quantifiers -- Parity Games Of Bounded Tree- And Clique-width -- Type Theory, Proof Theory And Implicit Computational Complexity -- Programming And Reasoning With Guarded Recursion For Coinductive Types -- The Computational Contents Of Ramified Corecurrence -- On The Dependencies Of Logical Rules -- On The Mints Hierarchy In First-order Intuitionistic Logic. Edited By Andrew Pitts. Foreword......Page 6 Preface......Page 8 Organization......Page 9 Contents......Page 12 Invited Talk......Page 15 1 Introduction......Page 16 2 Linear Logic and Session Types......Page 17 3 Categorical Truth......Page 20 4 Adjoint Logic......Page 22 5 Polarized Logic......Page 26 6 Recovering Synchronous Communication......Page 28 7 Synthesis in Polarized Adjoint Logic......Page 29 8 Sequent Calculus for Polarized Adjoint Logic......Page 32 9 Conclusion......Page 33 References......Page 34 Semantics of Programming Languages I......Page 36 1 Introduction......Page 37 2 Preliminaries......Page 39 3 Angelic and Demonic Nondeterminism......Page 40 4 Hoare Formulas and Their Meaning......Page 43 5 A Hoare Calculus for While Game Schemes......Page 45 6 Operational Model and Complexity......Page 48 7 A Complete Hoare-Style Calculus for Synthesis......Page 49 8 Discussion and Conclusion......Page 51 References......Page 52 1 Introduction......Page 53 2 The Relational Model of Linear Logic......Page 56 3 Fixpoint Operators in Models of Linear Logic......Page 57 4 A Fixpoint Operator in the Relational Semantics......Page 60 5 Infinitary Exponentials......Page 62 7 The Coloured Exponential Modality......Page 64 8 The Inductive-Coinductive Fixpoint Operator Y......Page 65 References......Page 66 1 Introduction......Page 68 2.1 PCF......Page 70 2.2 Innocent Strategies for PCF......Page 72 2.3 Computing Operations on Strategies by nbe......Page 74 3.1 A Semantic Domain......Page 76 3.2 Soundness for Conversion......Page 77 3.3 Computational Adequacy......Page 78 4 Game Semantics of PCF Based on nbe......Page 80 References......Page 81 1 Introduction......Page 83 2 Mathematical Foundations......Page 85 3 Loops......Page 88 4 The Programming Language......Page 91 5 Priorities......Page 94 References......Page 95 Categorical Models and Logics......Page 96 1 Introduction......Page 97 2 Preliminaries on Distributions and Convex Sets......Page 98 3 The Cancellation Property for Convex Sets......Page 100 4 Normalisation......Page 103 5 Effecti......Page 104 6 Conditional Probability......Page 109 7 Conclusions......Page 110 References......Page 111 1 Introduction......Page 112 2 Syntax......Page 114 3 Categorical Semantics......Page 120 4 Some Discrete Models: Monoidal Families......Page 123 5 Conclusions and Future Work......Page 124 References......Page 126 1 Introduction......Page 127 2 Preliminaries......Page 128 3 MainResult......Page 134 5 Decidability of Weighted Language Equivalence......Page 136 References......Page 138 1 Introduction......Page 143 2 From the Topos of Trees to Kripke Frames......Page 145 3 The Sequent Calculus SKMlin for KMlin......Page 147 4 Terminating Proof Search for KM......Page 154 5 Related Work......Page 155 References......Page 156 Modal and Temporal Logics......Page 158 1 Introduction......Page 159 2 Preliminaries......Page 161 3 Forgetful Logics......Page 162 4 Examples......Page 164 5 Forgetful Logics for Monads......Page 166 6 Determinization......Page 167 7 Logics Whose Mates are Isomorphisms......Page 170 References......Page 173 1 Introduction......Page 175 2 Preliminaries......Page 177 3 Expressiveness Issues......Page 181 4 Model-Checking against......Page 185 5 Discussion......Page 188 References......Page 189 Concurrent, Probabilisticand Timed Systems......Page 191 1 Introduction......Page 192 2 Preliminaries......Page 194 3 Semi-Markov Chains and Trace Distance......Page 195 4 Trace Distance and Probabilistic Model Checking......Page 196 5 General Convergence Criteria......Page 199 6 An Approximation Algorithm......Page 202 7 Conclusions and Future Work......Page 205 References......Page 206 1 Introduction......Page 207 2 Preliminaries......Page 209 3 Expressiveness and Decidability......Page 213 4 Integer HPAs......Page 219 5 Conclusions......Page 220 References......Page 221 1 Introduction......Page 222 2 Transition Systems......Page 223 3 Notions of Knowledge......Page 224 4 Application of Knowledge......Page 229 5 Implementation of Knowledge Using Bounded Memory......Page 230 6 Conclusions......Page 235 References......Page 236 1 Introduction......Page 237 2 Preliminaries......Page 238 3.1 Non-recursive Process Combinators......Page 241 3.2 Distance between Non-recursive Processes......Page 242 3.3 Compositional Reasoning Over Non-recursive Processes......Page 244 4.1 Recursive Process Combinator......Page 245 4.2 Distance between Recursive Processes......Page 246 4.3 Compositional Reasoning Over Recursive Processes......Page 247 5 Application......Page 248 References......Page 251 Semantics of ProgrammingLanguages II......Page 253 1 Introduction......Page 254 2 Preliminaries......Page 256 3.1 Characterising P-Strict......Page 260 3.2 Deciding Observational Equivalence of......Page 261 4.1 Fragment Definition......Page 263 4.2 Deciding Observation Equivalence......Page 264 5 Undecidable Fragments......Page 265 6 Conclusion......Page 266 References......Page 268 1 Introduction......Page 269 2 RefML and GroundML......Page 270 3 Trace Semantics......Page 271 3.1 Game-Like Definitions......Page 272 3.3 Interactive Reduction......Page 274 3.5 Interpretation of Terms......Page 277 4 A Correspondence between Trace and Game Denotations......Page 278 5.1 Ground-refererences Terms of RefML and P-visible Strategies......Page 280 5.2 Full Abstraction for GroundML......Page 281 6 Discussion and Future Work......Page 282 References......Page 283 1 Introduction......Page 284 2 The Language Fμ,⊕......Page 285 3 Observations and Biorthogonality......Page 287 4 Logical, CIU and Contextual Approximation Relations......Page 289 5 Examples......Page 293 6 Extension to References......Page 295 7 Conclusion......Page 297 References......Page 298 Automata, Games, Verification......Page 300 1 Introduction......Page 301 2 Preliminaries......Page 302 3 Fundamentals of Minimisation......Page 305 4 Minimisation Algorithms......Page 308 5 Decision Problem......Page 310 6 Minimal Consistent Multiplicity Automaton......Page 312 References......Page 314 1 Introduction......Page 316 2 Robust Multidimensional Mean-Payoff Games......Page 317 3 Reduction from the Halting Problem and Informal Proof of Correctness......Page 318 4 Detailed Proof......Page 324 References......Page 330 1 Introduction......Page 332 2.2 Modelling via Networks of Timed Automata......Page 333 2.3 Weighted Graph Formulation......Page 334 3.1 The Construction......Page 335 3.2 The Proof of Proposition 3......Page 339 References......Page 344 1 Introduction......Page 347 2 Preliminaries......Page 350 3 Type Systems for wMSOL......Page 352 4 Models for Weak Automata......Page 355 5 From Models to Type Systems......Page 358 6 Conclusions......Page 359 References......Page 360 Logical Aspects of ComputationalComplexity......Page 362 1 Introduction......Page 363 2 Background......Page 365 3 From Local Games to 3-Pebble Games......Page 367 4 MainResults......Page 369 5 Linear Functions......Page 372 6 Counterexample......Page 373 7 Conclusion and Future Work......Page 374 References......Page 375 A Appendix......Page 376 1 Introduction......Page 377 2 Preliminaries......Page 378 3 Quantifier Elimination and a Decision Procedure......Page 380 4 Automata Based Decision Procedure......Page 385 References......Page 390 1 Introduction......Page 392 2 Preliminaries......Page 393 3 Parse Trees......Page 397 4 Parity Games of Bounded Tree-Width......Page 398 5 Parity Games of Bounded Clique-Width......Page 404 References......Page 405 Type Theory, Proof Theory andImplicit Computational Complexity......Page 407 1 Introduction......Page 408 2 Guardedλ-calculus......Page 410 3 Denotational Semantics and Normalisation......Page 414 4 Logic for Guarded Lambda Calculus......Page 417 5 Behavioural Differential Equations in......Page 420 6 Discussion......Page 421 References......Page 422 1 Introduction......Page 423 2 Finite Transducers on Streams......Page 425 3 Corecurrence......Page 428 4 Ramified Corecurrence......Page 430 Type system RC for the primitive corecursive functions......Page 431 5 Log-Space Computation over Finite Streams......Page 433 References......Page 435 1 Introduction......Page 437 2.1 Linear Logic and Proof Nets......Page 439 2.2 Correctness Criteria......Page 440 2.3 Danos-Regnier Criterion......Page 441 2.4 Contractibility......Page 442 3 On the Three Faces of Contractibility......Page 443 3.1 Contractibilty and Sequentialization......Page 444 3.3 Towards Dependency Graphs......Page 445 3.4 DepGraph Criterion......Page 446 3.5 Comparing the Two Notions of Dependency Graphs......Page 448 4 On the Order of Introduction of Connectives in Sequentializations......Page 449 5 Conclusion......Page 450 References......Page 451 1 Introduction......Page 452 2 Preliminaries......Page 454 3 Classes......Page 456 4completeness for......Page 461 5 Conclusion......Page 465 References......Page 466 Author Index......Page 467