## Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, Volume 18Thisvolumecontainspapersselectedforpresentationatthe2004AnnualConf- enceoftheEuropeanAssociationforComputerScienceLogic, heldonSeptember 20-24, 2004 in Karpacz, Poland. The CSL conference series started as the International Workshops on C- puterScienceLogic, andthen, after?vemeetings, becametheAnnualConference of the European Association for Computer Science Logic. This conference was the 18th meeting, and the 13th EACSL conference. Altogether 99 abstracts were submitted, followed by 88 papers. Each of these paperswasrefereedbyatleastthreereviewers.Then, afteratwo-weekelectronic discussion, the Programme Committee selected 33 papers for presentation at the conference. Apart from the contributed papers, the Committee invited lectures from Albert Atserias, Martin Hyland, Dale Miller, Ken McMillan and Pawel Urzyczyn. WewouldliketothankallPCmembersandthesubrefereesfortheirexcellent work. The electronic PC meeting would not be possible without good software support. We decided to use the GNU CyberChair system, created by Richard van de Stadt, and we are happy with this decision. We also would like to thank Micha l Moskal who installed and ran CyberChair for us. Finally, we would like to thank ToMasz Wierzbicki, who helped with the preparation of this volume. We gratefully acknowledge ?nancial support for the conference received from the Polish Committee for Scienti?c Research, and Wroc law University. July 2004 Jerzy Marcinkowski and Andrzej Tarlecki Organization CSL 2004 was organized by the Institute of Computer Science, Wrocla w University. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Notions of AverageCase Complexity for Random 3SAT | 1 |

Classical Propositional Calculus | 6 |

Checking | 22 |

An Abstract | 24 |

My UnFavourite Things | 25 |

On Nash Equilibria in Stochastic Games | 26 |

A Bounding Quantiﬁer | 41 |

Parity and Exploration Games on Inﬁnite Graphs | 56 |

Towards Mechanized Program Veriﬁcation with Separation Logic | 250 |

A Functional Scenario for Bytecode Veriﬁcation of Resource Bounds | 265 |

Proving Abstract Noninterference | 280 |

Intuitionistic LTL and a New Characterization of Safety and Liveness | 295 |

The Balanced Case | 310 |

Parameterized Model Checking of RingBased Message Passing Systems | 325 |

PSPACE | 340 |

Theories with Induction | 355 |

Integrating Equational Reasoning into InstantiationBased Theorem Proving | 71 |

GoalDirected Methods for Lukasiewicz Logic | 85 |

A General Theorem on Termination of Rewriting | 100 |

Predicate Transformers and Linear Logic | 115 |

Structures for Multiplicative Cyclic Linear Logic | 130 |

with Units | 145 |

The Boundary Between Decidability and Undecidability for TransitiveClosure Logics | 160 |

GameBased Notions of Locality over Finite Models | 175 |

Fixed Points of Type Constructors and Primitive Recursion | 190 |

On the Building of Affine Retractions | 205 |

with Pairing | 220 |

A Dependent Type Theory with Names and Binding | 235 |

Logical Characterizations of PSPACE | 370 |

The Logic of the Partial λCalculus with Equality | 385 |

Complete Lax Logical Relations for Cryptographic LambdaCalculi | 400 |

Subtyping Union Types | 415 |

Pfaffian Hybrid Systems | 430 |

Axioms for Delimited Continuations in the CPS Hierarchy | 442 |

Set Constraints on Regular Terms | 458 |

Unsound Theorem Proving | 473 |

A Space Efficient Implementation of a Tableau Calculus for a Logic with a Constructive Negation | 488 |

Automated Generation of Analytic Calculi for Logics with Linearity | 503 |

518 | |

### Other editions - View all

Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual ... Jerzy Marcinkowski No preview available - 2014 |

### Common terms and phrases

abstract interpretation abstract non-interference algebra algorithm applied atomic axioms binary relation bisimulation bounded cell clauses closure complete Computer Science consider constraints construction constructors context CPS translation cut-elimination define deﬁned deﬁnition denote dependent type theory derivation equations equivalent example exists finite ﬁrst first-order formula function symbol given graph Heyting algebra Hoare logic hypersequent inference infinite interpretation intuitionistic isomorphism lambda calculus language Lemma linear logic LNCS logical relations model checking monoidal morphisms multiset Nash equilibria nodes notion obtained operator pair Parity partial payoff pcccs player polynomial problem proof proof nets Proposition PSPACE quantifier reachability recursion result rule safety and liveness satisfiability semantics sequent calculus stochastic games strategy structure subterm theorem proving transition tree type theory variables verification vertex vertices well-founded winning