CSL
2006
Springer
14 years 3 months ago
2006
Springer
Separation Logic is a sub-structural logic that supports local reasoning for imperative programs. It is designed to elegantly describe sharing and aliasing properties of heap struc...
CSL
2006
Springer
14 years 3 months ago
2006
Springer
Abstract. Expansions of the natural number ordering by unary predicates are studied, using logics which in expressive power are located between first-order and monadic second-order...
CSL
2006
Springer
14 years 3 months ago
2006
Springer
For a two-variable formula (X, Y ) of Monadic Logic of Order (MLO) the Church Synthesis Problem concerns the existence and construction of an operator Y = F(X) such that (X, F(X)) ...
CSL
2006
Springer
14 years 3 months ago
2006
Springer
CSL
2006
Springer
14 years 3 months ago
2006
Springer
Abstract. In [6] J. Laird has shown that an infinitary sequential extenPCF has a fully abstract model in his category of locally boolean domains (introduced in [8]). In this paper ...
CSL
2006
Springer
14 years 3 months ago
2006
Springer
Based on natural deduction, Pure Type Systems (PTS) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent...
CSL
2006
Springer
14 years 3 months ago
2006
Springer
Game quantification is an expressive concept and has been studied in model theory and descriptive set theory, especially in relation to infinitary logics. Automatic structures on t...
CSL
2006
Springer
14 years 3 months ago
2006
Springer
The synthesis of reactive systems requires the solution of two-player games on graphs with -regular objectives. When the objective is specified by a linear temporal logic formula o...
CSL
2006
Springer
14 years 3 months ago
2006
Springer
Abstract. Bisimilarity and weak bisimilarity are canonical notions of equivalence between processes, which are defined co-inductively, but may be approached
CSL
2006
Springer
14 years 3 months ago
2006
Springer
We introduce a new class of multiplicative proof nets, J-proof nets, which are a typed version of Faggian and Maurel's multiplicative L-nets. In J-proof nets, we can character...