This book constitutes the refereed proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2010, held in Paphos, Cyprus, in March 2010, as part of ETAPS 2010, the European Joint Conferences on Theory and Practice of Software. The 25 revised full papers presented together with the abstract of the keynote lecture were carefully reviewed and selected from 86 full paper submissions. The papers are organized in topical sections on semantics of programming languages, probabilistic and randomised computation, concurrency and process theory, modal and temporal logics, verification, categorical and coalgebraic methods, as well as lambda calculus and types.
Author(s): Colin Stirling (auth.), Luke Ong (eds.)
Series: Lecture Notes in Computer Science 6014 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 389
Tags: Mathematical Logic and Formal Languages; Computation by Abstract Devices; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Software Engineering
Front Matter....Pages -
Introduction to Decidability of Higher-Order Matching....Pages 1-1
A Semantic Foundation for Hidden State....Pages 2-17
Linearly-Used Continuations in the Enriched Effect Calculus....Pages 18-32
Block Structure vs. Scope Extrusion: Between Innocence and Omniscience....Pages 33-47
Completeness for Algebraic Theories of Local State....Pages 48-63
Fair Adversaries and Randomization in Two-Player Games....Pages 64-78
Retaining the Probabilities in Probabilistic Testing Theory....Pages 79-93
Forward Analysis of Depth-Bounded Processes....Pages 94-108
Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization....Pages 109-127
Parameterised Multiparty Session Types....Pages 128-145
On the Relationship between Spatial Logics and Behavioral Simulations....Pages 146-160
An Easy Completeness Proof for the Modal μ -Calculus on Finite Trees....Pages 161-175
When Model-Checking Freeze LTL over Counter Machines Becomes Decidable....Pages 176-190
Model Checking Is Static Analysis of Modal Logic....Pages 191-205
Counting CTL ....Pages 206-220
Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems....Pages 221-236
Toward a Compositional Theory of Leftist Grammars and Transformations....Pages 237-251
Degrees of Lookahead in Regular Infinite Games....Pages 252-266
Reachability Analysis of Communicating Pushdown Systems....Pages 267-281
The Complexity of Synchronous Notions of Information Flow Security....Pages 282-296
Monads Need Not Be Endofunctors....Pages 297-311
CIA Structures and the Semantics of Recursion....Pages 312-327
Coalgebraic Correspondence Theory....Pages 328-342
Untyped Recursion Schemes and Infinite Intersection Types....Pages 343-357
Solvability in Resource Lambda-Calculus....Pages 358-373
A Hierarchy for Delimited Continuations in Call-by-Name....Pages 374-388
Back Matter....Pages -
