This special issue contains extended versions of selected papers presented at FoSSaCS 2010, the 13th International Conference on Foundations of Software Science and Computational Structures, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2010, 20 - 28 March 2010, Paphos, Cyprus.

FoSSaCS 2010 received 86 full paper submissions; of these 25 were selected for presentation at the Conference and for publication in the proceedings (LNCS 6014).

After the Conference, the FoSSaCS 2010 Programme Committee identified six strong papers; and their authors were invited to submit full and extended versions to the special issue. All six papers that appear in this special issue have been refereed to the usual standards of LMCS.

The selected papers reflect the high quality of the Conference and represent a wide range of topics. The first two concern the theory of verification. In Degrees of Lookahead in Regular Infinite Games, Michael Holtmann, Łukasz Kaiser and Wolfgang Thomas study regular infinite games whereby the second player may take advantage of finite lookahead, i.e., postponing a move for a finite number of steps. They consider the decidability of solvability of regular infinite games by strategies of various types of finite lookahead, and the reducibility of a given strategy of one type to another.

The other verification paper, Reachability Analysis of Communicating Pushdown Systems by Alexander Heussner, Jérôme Leroux, Anca Muscholl and Grégoire Sutre, is about the reachability analysis of pushdown systems that communicate asynchronously over reliable FIFO channels. Restricted to systems of eager runs (i.e., runs where messages are either received immediately after being sent, or never received), they identify communication topologies that guarantee decidability of the reachability problem, and present algorithms for bounded context analysis of these systems.

The remaining four papers cover various aspects of semantics. In Linear-use CPS translations in the Enriched Effect Calculus, Jeff Egger, Rasmus Miøgelberg and Alex Simpson introduce the enriched effect calculus (EEC) as an extension of Moggi's computational metalanguage with linear logic primitives. The paper explores the EEC as a target language for CPS translations in which the typing of the translations enforces the linear usage of continuations. They prove that the generic self-translation of EEC is involutive up to isomorphism, and several full completeness results are obtained as corollaries.

In Parameterised Multiparty Session Types, Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri and Raymond Hu propose a dependent type theory for multiparty sessions which can statically guarantee type-safe and deadlock-free multiparty interactions among parameterised processes. The main technical result is the termination of type checking with both multiparty session types and recursive types.

Stefan Milius, Lawrence Moss and Daniel Schwencke study the semantics of recursive function definitions in Abstract GSOS Rules and a Modular Treatment of Recursive Definitions. They give a uniform account of the unique solvability of recursive specifications using GSOS rule-based algebraic operations on terminal coalgebras. Their semantic framework supports a modularity principle: solutions of recursive definitions in terminal coalgebras may be used in subsequent recursive definitions which still have unique solutions.

Last but not least, the paper by Thosten Altenkirch, James Chapman and Tarmo Uustalu, Monads need not be endofunctors, is an advance in category theory. They introduce a generalisation of monads, called relative monads, which allow for underlying functors between different categories. They show that the Kleisli and Eilenberg-Moore constructions carry over to relative monads and are related to relative adjunctions. Arrows are also an instance of relative monads.

We would like to thank the authors of the papers for their contributions, the members of the FoSSaCS 2010 Programme Committee and the referees for their reviews, and the managing and executive editors of LMCS for their help and guidance throughout the review process.