# Selected Papers of the Conference "Computer Science Logic 2006"

2006

Editors: Zoltan Esik, R. Ramanujam

### 1. A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of<br> Automata

Model checking properties are often described by means of finite automata. Any particular such automaton divides the set of infinite trees into finitely many classes, according to which state has an infinite run. Building the full type hierarchy upon this interpretation of the base type gives a […]

### 2. Relating two standard notions of secrecy

Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data s. Reachability-based secrecy means that s should never be disclosed while equivalence-based secrecy states that two executions of a protocol with distinct instances for s […]

### 3. Algorithms for Omega-Regular Games with Imperfect Information

We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller […]

### 4. The Church Synthesis Problem with Parameters

For a two-variable formula &psi;(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 &psi;(X,F(X)) is universally valid over Nat. Büchi and Landweber proved that the Church synthesis problem is decidable; […]

### 5. Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic

In a previous work Baillot and Terui introduced Dual light affine logic (DLAL) as a variant of Light linear logic suitable for guaranteeing complexity properties on lambda calculus terms: all typable terms can be evaluated in polynomial time by beta reduction and all Ptime functions can be […]

### 6. Normalization of IZF with Replacement

ZF is a well investigated impredicative constructive version of Zermelo-Fraenkel set theory. Using set terms, we axiomatize IZF with Replacement, which we call \izfr, along with its intensional counterpart \iizfr. We define a typed lambda calculus $\li$ corresponding to proofs in \iizfr according to […]

### 7. Semi-continuous Sized Types and Termination

Some type-based approaches to termination use sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is visible in the type system that recursive calls occur just at a smaller size. This approach is only sound […]

### 8. Universal Structures and the logic of Forbidden Patterns

Forbidden Patterns Problems (FPPs) are a proper generalisation of Constraint Satisfaction Problems (CSPs). However, we show that when the input is connected and belongs to a class which has low tree-depth decomposition (e.g. structure of bounded degree, proper minor closed class and more generally […]