CSL
2007
Springer
14 years 6 months ago
2007
Springer
A game semantics of the (−−∗, →)-fragment of the logic of bunched implications, BI, is presented. To date, categorical models of BI have been restricted to two kinds: funct...
CSL
2007
Springer
14 years 6 months ago
2007
Springer
The question of the exact complexity of solving parity games is one of the major open problems in system verification, as it is equivalent to the problem of model-checking the mod...
CSL
2007
Springer
14 years 6 months ago
2007
Springer
We provide a new correctness criterion for unit-free MLL proof structures and MELL proof structures with units. We prove that deciding the correctness of a MLL and of a MELL proof ...
CSL
2007
Springer
14 years 6 months ago
2007
Springer
We give a fully abstract game model for Idealized Algol with non-local control flow. In contrast to most previous papers on game semantics, we do not need to include the bad-varia...
CSL
2007
Springer
14 years 6 months ago
2007
Springer
We show how to extract classical programs expressed in Krivine λc-calculus from proof-terms built in a proof-irrelevant and classical version of the calculus of constructions with...
CSL
2007
Springer
14 years 6 months ago
2007
Springer
Abstract. Probably the most significant result concerning cut-free sequent calculus proofs in linear logic is the completeness of focused proofs. This completeness theorem has a n...
CSL
2007
Springer
14 years 6 months ago
2007
Springer
A focused proof system provides a normal form to cut-free proofs that structures the application of invertible and non-invertible inference rules. The focused proof system of Andre...
CSL
2007
Springer
14 years 6 months ago
2007
Springer
Normal form bisimulation is a powerful theory of program equivalence, originally developed to characterize L´evy-Longo tree equivalence and Boehm tree equivalence. It has been ada...
CSL
2007
Springer
14 years 6 months ago
2007
Springer
Automata on infinite objects were the key to the solution of several fundamental decision problems in mathematics and logic. Today, automata on infinite objects are used for form...
CSL
2007
Springer
14 years 6 months ago
2007
Springer
Abstract. We present a method of integrating linear rational arithmetic into superposition calculus for first-order logic. One of our main results is completeness of the resulting...