Special Issue for the 13th International Conference on "FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES" FOSSACS 2010

PDF

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.

Luke Ong
FoSSaCS 2010 Programme Chair, and LMCS Special Issue Guest Editor

1. Reachability Analysis of Communicating Pushdown Systems

Alexander Heussner ; Jérôme Leroux ; Anca Muscholl ; Grégoire Sutre.
The reachability analysis of recursive programs that communicate asynchronously over reliable FIFO channels calls for restrictions to ensure decidability. Our first result characterizes communication topologies with a decidable reachability problem restricted to eager runs (i.e., runs where messages are either received immediately after being sent, or never received). The problem is EXPTIME-complete in the decidable case. The second result is a doubly exponential time algorithm for bounded context analysis in this setting, together with a matching lower bound. Both results extend and improve previous work from La Torre et al.

2. Degrees of Lookahead in Regular Infinite Games

Michael Holtmann ; Lukasz Kaiser ; Wolfgang Thomas.
We study variants of regular infinite games where the strict alternation of moves between the two players is subject to modifications. The second player may postpone a move for a finite number of steps, or, in other words, exploit in his strategy some lookahead on the moves of the opponent. This captures situations in distributed systems, e.g. when buffers are present in communication or when signal transmission between components is deferred. We distinguish strategies with different degrees of lookahead, among them being the continuous and the bounded lookahead strategies. In the first case the lookahead is of finite possibly unbounded size, whereas in the second case it is of bounded size. We show that for regular infinite games the solvability by continuous strategies is decidable, and that a continuous strategy can always be reduced to one of bounded lookahead. Moreover, this lookahead is at most doubly exponential in the size of a given parity automaton recognizing the winning condition. We also show that the result fails for non-regular gamesxwhere the winning condition is given by a context-free omega-language.

3. Linear-use CPS translations in the Enriched Effect Calculus

Jeff Egger ; Rasmus Ejlers Møgelberg ; Alex Simpson.
The enriched effect calculus (EEC) is an extension of Moggi's computational metalanguage with a selection of primitives from linear logic. This paper explores the enriched effect calculus as a target language for continuation-passing-style (CPS) translations in which the typing of the translations enforces the linear usage of continuations. We first observe that established call-by-value and call-by name linear-use CPS translations of simply-typed lambda-calculus into intuitionistic linear logic (ILL) land in the fragment of ILL given by EEC. These two translations are uniformly generalised by a single generic translation of the enriched effect calculus into itself. As our main theorem, we prove that the generic self-translation of EEC is involutive up to isomorphism. As corollaries, we obtain full completeness results, both for the generic translation, and for the original call-by-value and call-by-name translations.

4. Parameterised Multiparty Session Types

Pierre-Malo Denielou ; Nobuko Yoshida ; Andi Bejleri ; Raymond Hu.
For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from Gödel's System T to express a wide range of communication patterns while keeping type checking decidable. To type individual distributed processes, a parameterised global type is projected onto a generic generator which represents a class of all possible end-point types. We prove the termination of the type-checking algorithm in the full system with both multiparty session types and recursive types. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.

5. Abstract GSOS Rules and a Modular Treatment of Recursive Definitions

Stefan Milius ; Lawrence S Moss ; Daniel Schwencke.
Terminal coalgebras for a functor serve as semantic domains for state-based systems of various types. For example, behaviors of CCS processes, streams, infinite trees, formal languages and non-well-founded sets form terminal coalgebras. We present a uniform account of the semantics of recursive definitions in terminal coalgebras by combining two ideas: (1) abstract GSOS rules l specify additional algebraic operations on a terminal coalgebra; (2) terminal coalgebras are also initial completely iterative algebras (cias). We also show that an abstract GSOS rule leads to new extended cia structures on the terminal coalgebra. Then we formalize recursive function definitions involving given operations specified by l as recursive program schemes for l, and we prove that unique solutions exist in the extended cias. From our results it follows that the solutions of recursive (function) definitions in terminal coalgebras may be used in subsequent recursive definitions which still have unique solutions. We call this principle modularity. We illustrate our results by the five concrete terminal coalgebras mentioned above, e.\,g., a finite stream circuit defines a unique stream function.

6. Monads need not be endofunctors

Thosten Altenkirch ; James Chapman ; Tarmo Uustalu.
We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We show that the Kleisli and Eilenberg-Moore constructions carry over to relative monads and are related to relative adjunctions. Under reasonable assumptions, relative monads are monoids in the functor category concerned and extend to monads, giving rise to a coreflection between relative monads and monads. Arrows are also an instance of relative monads.