FOSSACS
2010
Springer
13 years 9 months ago
2010
Springer
FOSSACS
2010
Springer
14 years 2 months ago
2010
Springer
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 f...
FOSSACS
2010
Springer
14 years 2 months ago
2010
Springer
Abstract. The enriched effect calculus is an extension of Moggi's computational metalanguage with a selection of primitives from linear logic. In this paper, we present an ext...
FOSSACS
2010
Springer
14 years 2 months ago
2010
Springer
A new framework for higher-order program verification has been recently proposed, in which higher-order functional programs are modelled as higher-order recursion schemes and then ...
FOSSACS
2010
Springer
14 years 5 months ago
2010
Springer
Abstract. We study the semantic meaning of block structure using game semantics and introduce the notion of block-innocent strategies, which turns out to characterise call-by-value...
FOSSACS
2010
Springer
14 years 5 months ago
2010
Springer
We present a coinductive proof system for bisimilarity in transition systems specifiable in the de Simone SOS format. Our coinduction is incremental, in that it allows building in...
FOSSACS
2010
Springer
14 years 5 months ago
2010
Springer
Abstract. Spatial logics have been introduced to reason about distributed computation in models for concurrency. We first define a spatial logic for a general class of infinite-...
FOSSACS
2010
Springer
14 years 5 months ago
2010
Springer
Abstract. The reachability analysis of recursive programs that communicate asynchronously over reliable Fifo channels calls for restrictions to ensure decidability. We extend here ...
FOSSACS
2010
Springer
14 years 5 months ago
2010
Springer
Leftist grammars [Motwani et al., STOC 2000] are special semi-Thue systems where symbols can only insert or erase to their left. We develop a theory of leftist grammars seen as wor...
FOSSACS
2010
Springer
14 years 5 months ago
2010
Springer
Depth-bounded processes form the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. In this paper we develop an ade...