Selected Paper of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015)

Editors: Thomas Colcombet, Andrew M. Pitts, Daniele Varacca

This special issue contains extended versions of six papers presented at FoSSaCS 2015, the 18th 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 2015, London, UK, 11-18 April 2015.

The papers collected in this special issue were invited by the guest editors, taking into account the views of the Program Committee and expert reviewers expressed during the conference paper selection process. We are grateful to the authors of all the conference papers for their excellent submissions.

The papers selected for this special issue reflect the high level of the conference and represent a wide range of topics. They underwent a new and thorough reviewing and revision process, in accordance with the usual high standards of LMCS. We thank the authors and the reviewers for all their hard work producing the contents of this issue.

Thomas Colcombet, Andrew Pitts, Daniele Varacca
FoSSaCS 2015 Guest Editors

1. The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types

Clouston, Ranald ; Bizjak, Aleš ; Grathwohl, Hans Bugge ; Birkedal, Lars.
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by […]

2. Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism

Mamouras, Konstantinos.
We study a propositional variant of Hoare logic that can be used for reasoning about programs that exhibit both angelic and demonic nondeterminism. We work in an uninterpreted setting, where the meaning of the atomic actions is specified axiomatically using hypotheses of a certain form. Our […]

3. Coalgebraic trace semantics via forgetful logics

Klin, Bartek ; Rot, Jurriaan.
We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and tree automata, and the trace semantics of generative probabilistic systems. We provide a sufficient condition […]

4. Compositional bisimulation metric reasoning with Probabilistic Process Calculi

Gebler, Daniel ; Larsen, Kim G. ; Tini, Simone.
We study which standard operators of probabilistic process calculi allow for compositional reasoning with respect to bisimulation metric semantics. We argue that uniform continuity (generalizing the earlier proposed property of non-expansiveness) captures the essential nature of compositional […]

5. Typing weak MSOL properties

Salvati, Sylvain ; Walukiewicz, Igor.
We consider lambda-Y-calculus as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as the tree of calls to built-in operations. Weak monadic second-order logic (wMSOL) is well suited to express properties of such trees. We […]

6. Minimisation of Multiplicity Tree Automata

Kiefer, Stefan ; Marusic, Ines ; Worrell, James.
We consider the problem of minimising the number of states in a multiplicity tree automaton over the field of rational numbers. We give a minimisation algorithm that runs in polynomial time assuming unit-cost arithmetic. We also show that a polynomial bound in the standard Turing model would require […]