 Andreas Abel and Ralph Matthes
 Fixed Points of Type Constructors and Primitive Recursion
 For nested or heterogeneous datatypes, terminating recursion schemes
considered so far have been instances of iteration, excluding efficient
definitions of fixedpoint unfolding. Two solutions of this problem are
proposed: The first one is a system with equirecursive nonstrictly
positive type operators of arbitrary finite kinds, where fixedpoint
unfolding is computationally invisible due to its treatment on the level
of type equality. Positivity is ensured by a polarized kinding system, and
strong normalization is proven by a model construction based on saturated
sets. The second solution is a formulation of primitive recursion for
arbitrary type constructors of any rank. Although without positivity
restriction, the second system embeds — even operationally —
into the first one.
 Roberto M. Amadio, Solange CoupetGrimal, Silvano Dal
Zilio, and Line Jakubiec
 A Functional Scenario for Bytecode Verification of Resource
Bounds
 We
consider a scenario where (functional) programs in precompiled form
are exchanged among untrusted parties. Our contribution is a system of
annotations for the code that can be verified at load time so as to
ensure bounds on the time and space resources required for its
execution, as well as to guarantee the usual integrity properties.
Specifically, we define a simple stack machine for a firstorder
functional language and show how to perform type, size, and termination
verifications at the level of the bytecode of the machine. In
particular, we show that a combination of size verification based on
quasiinterpretations and of termination verification based on
lexicographic path orders leads to an explicit bound on the space
required for the execution.
 Marcelo Arenas, Pablo Barceló, and Leonid Libkin
 Gamebased Notions of Locality over Finite Models
 Locality notions in logic say that the truth value of a formula
can be determined locally, by looking at the isomorphism type of a
small neighborhood of its free variables. Such notions have proved to
be useful in many applications. They all, however, refer to isomorphism of
neighborhoods, which most local logics cannot test. A more relaxed notion
of locality says that the truth value of a formula is determined
by what the logic itself can say about that small neighborhood. Or,
since most logics are characterized by games, the truth value of a
formula is determined by the type, with respect to a game, of that small
neighborhood. Such gamebased notions of locality can often be applied
when traditional isomorphismbased locality cannot. Our goal is to study
gamebased notions of locality. We work with an abstract view of games
that subsumes games for many logics. We look at three, progressively
more complicated locality notions. The easiest requires only very mild
conditions on the game and works for most logics of interest. The
other notions, based on Hanf's and Gaifman's theorems, require more
restrictions. We state those restrictions and give examples of logics
that satisfy and fail the respective gamebased notions of locality.
 Alessandro Avellone, Camillo Fiorentini, Guido
Fiorino, and Ugo Moscato
 An Efficent Implementation of a Tableau Calculus for a Logic with
a Constructive Negation
 A tableau calculus for a logic with constructive negation and an
implementation of the related decision procedure is presented. This logic
is an extension of Nelson logic and it has been used in the framework of
program verification and timing analysis of combinatorial circuits. The
decision procedure is tailored to shrink the search space of proofs and
it is proved correct by using a semantical technique and it has been
implemented in C++ language.
 Mikolaj Bojanczyk
 A Bounding Quantifier
 The logic MSOL+B is defined, by extending monadic
secondorder logic on the infinite binary tree with a new bounding
quantifier B. In this logic, a formula
BX.φ(X)
states that there is a finite bound on the size of sets satisfying
φ(X). Satisfiability is proved decidable for two fragments of
MSOL+B: formulas of the form ¬BX.φ(X),
with φ a Bfree formula; and formulas built from
Bfree formulas by nesting B, ∃, ∨
and ∧.
 Krishnendu Chatterjee,
Rupak Majumdar, and Marcin Jurdzinski
 On Nash Equilibria in Stochastic Games
 We study infinite stochastic games played by nplayers on a
finite graph with goals given by sets of infinite traces. The games
are stochastic (each player simultaneously and independently
chooses an action at each round, and the next state is determined
by a probability distribution depending on the current state and the
chosen actions), infinite (the game continues for an infinite
number of rounds), nonzero sum (the players' goals are not
necessarily conflicting), and undiscounted. We show that if each
player has a reachability objective, that is, if the goal for
each player i is to visit some subset R_{i}
of the states, then
there exists an εNash equilibrium in memoryless strategies,
for every ε>0. We study the complexity of finding such Nash
equilibria. Given an nplayer reachability game, we show for every
fixed ε, the value of some memoryless εNash equilibrium
can be εapproximated in NP. However, for a vector of values
(v_{1},...,v_{n}),
it is NPcomplete to determine if there exists a
pure, memoryless εNash equilibrium where each player gets payoff
at least v_{i}. Our techniques for general nonzero
sum games also yield NP ∩ coNP εapproximation
algorithms for zerosum reachability
games, improving the previously known EXPTIME bound. We study the important
subclass of nplayer perfectinformation or turnbased
probabilistic games, where at each state at most one player has a
nontrivial choice of moves. For turnbased probabilistic games, we show
the existence of εNash equilibria in pure strategies for
games where the objective of player i is a Borel set
B_{i} of
infinite traces. For the special case of ωregular objectives,
we show exact Nash equilibria exist, and can be computed in NP when the
ωregular objectives are expressed as parity objectives.
 Agata Ciabattoni
 Automated Generation of Analytic Calculi for Logics with
Linearity
 We show how to automatically generate analytic hypersequent
calculi for a large class of logics containing the linearity axiom
(lin) (A → B) ∨ (B → A) starting from existing analytic calculi for
the corresponding logics without (lin). As a corollary, we define an
analytic hypersequent calculus for Strict Monoidal Tnorm based Logic
SMTL.
 Andrés CordónFranco, Alejandro
FernándezMargarit, and F. Félix LaraMartín
 Provably Total Primitive Recursive Functions: Theories with
Induction

A natural example of a function algebra is R(T), the class of
provably total computable functions (p.t.c.f.) of a theory T in the
language of first order Arithmetic. In this paper a simple
characterization of that kind of function algebras is obtained. This
provides a useful tool for studying the class of primitive recursive
functions in R(T). We prove that this is the class of p.t.c.f. of
the theory axiomatized by the induction scheme restricted to (parameter
free) Δ_{1}(T)formulas
(i.e., Σ_{1}formulas which are equivalent in
T to Π_{1}formulas). Moreover, if T is a sound theory and
proves that exponentiation is a total function, we characterize the
class of primitive recursive functions in R(T) as a function
algebra described in terms of bounded recursion (and composition).
Extensions of this result are related to open problems on complexity
classes. We also discuss an application to the problem on the
equivalence between (parameter free) Σ_{1}collection and
(uniform) Δ_{1}induction schemes in Arithmetic. The
proofs lean upon axiomatization and conservativeness properties of the
scheme of Δ_{n+1}(T)induction and its parameter
free version.
 Jeremy E. Dawson and Rajeev Goré
 A General Theorem on Termination of Rewriting
 We reexpress our theorem on the strongnormalisation
of display calculi
as a theorem about the wellfoundedness of a certain ordering on
firstorder terms, thereby allowing us to prove the termination of
systems of rewrite rules. We first show how to use our theorem to prove
the wellfoundedness of the lexicographic ordering, the multiset
ordering and the recursive path ordering. Next, we give examples of
systems of rewrite rules which cannot be handled by these methods but
which can be handled by ours. Finally, we show that our method can also
prove the termination of the KnuthBendix ordering and of dependency
pairs.
 Philippe de Groote and Sylvain Salvati
 Higherorder Matching in the Linear λcalculus with
Pairing

We prove that higherorder matching in the linear λcalculus
with pairing is decidable. We also establish its NPcompleteness under
the assumption that the righthand side of the equation to be solved is
given in normal form.
 Pietro Di Gianantonio
 Structures for Multiplicative Cyclic Linear Logic: Deepness vs
Cyclicity

The aim of this work is to give an alternative presentation for the
multiplicative fragment of Yetter's cyclic linear logic. The new
presentation is inspired by the calculus of structures, and has the
interesting feature of avoiding the cyclic rule. The main point in
this work is to show how cyclicity can be substituted by deepness,
i.e., the possibility of applying an inference rule at any point of
a formula. We finally derive, through a new proof technique, the
cut elimination property of the calculus.
 E. Allen Emerson and Vineet Kahlon
 Parameterized Model Checking of Ringbased Message Passing
Systems

The Parameterized Model Checking Problem (PMCP) is to decide whether a
temporal property holds for a uniform family of systems comprised of
finite, but arbitrarily many, copies of a template process.
Unfortunately, it is undecidable in general. In this paper, we consider
the PMCP for systems comprised of processes arranged in a ring that
communicate by passing messages via tokens whose values can be updated
at most a bounded number of times. Correctness properties are expressed
using the stutteringinsensitive temporal logic LTL\X. For
bidirectional rings we show how to reduce reasoning about rings with an
arbitrary number of processes to rings with up to a certain finite
“cutoff” number of processes. This immediately yields
decidability of the PMCP at hand. We go on to show that for
unidirectional rings small cutoffs can be achieved, making the decision
procedure provably efficient. As example applications, we consider
protocols for the leader election problem.
 Harald Ganzinger and Konstantin Korovin
 Integrating Equational Reasoning into Instantiationbased Theorem
Proving

In this paper we present a method for integrating equational reasoning
into instantiationbased theorem proving. The method employs a
satisfiability solver for ground equational clauses together with an
instance generation process based on an ordered paramodulation type
calculus for literals. The completeness of the procedure is proved
using the the model generation technique, which allows us to justify
redundancy elimination based on appropriate orderings.
 Roberto Giacobazzi and Isabella Mastroeni
 Proving Abstract NonInterference
 In this paper we introduce a compositional proofsystem for certifying
abstract noninterference in programming languages. Certifying abstract
noninterference means proving that nounauthorized flow of information
is observable by the attacker from confidential to public data. The
properties of the computation that an attacker may observe are specified in
an abstract domain. Assertions specify the secrecy of a program relatively
to the given attacker and the proofsystem specifies how these assertions
can be composed in a syntaxdirected á la Hoare
deduction of secrecy.
We prove that the proofsystem is sound relatively to the standard semantics
of an imperative programming language with nondeterministic choice. This
provides a sound proofsystem for both certifying secrecy in languagebased
security and deriving attackers which do not violate secrecy inductively
on program's syntax.
 Hugo Gimbert
 Parity and Exploration Games on Infinite Graphs
 This paper examines two players' turnbased perfectinformation
games played on infinite graphs. Our attention is focused on the class of
games where winning conditions are boolean combinations of the following
two conditions: (1) the first one states that an infinite
play is won
by player 0 if during the play infinitely many different vertices were
visited, (2) the second one is the well known parity condition generalized
to a countable number of priorities. We show that, in most cases, both
players have positional winning strategies and we characterize their
respective winning sets. In the special case of pushdown graphs, we use
these results to show that the sets of winning positions are regular
and we show how to compute them as well as positional winning strategies
in exponential time.
 Jean GoubaultLarrecq, Slawomir
Lasota, David Nowak, and Yu Zhang
 Complete Lax Logical Relations for Cryptographic
LambdaCalculi
 Security properties are usually expressed using notions of contextual
equivalence, to which logical relations are a powerful proof technique in
typed lambda calculi, e.g.,
Sumii and Pierce's logical relation for their
cryptographic lambdacalculus. We clarify Sumii and Pierce's approach,
using a cryptographic version of Moggi's monadic lambdacalculus as
framework, and show that their logical relations can be recovered by a
notion of lax logical relations. We also explore the question of fresh
names by using Stark's name creation monad and define logical relations
which are lax at encryption and function types but strict (nonlax)
at monad types. We show that they are sound and complete for contextual
equivalence at all types.
 Pierre Hyvernat
 Predicate Transformers and Linear Logic: yet another Denotational
Model
 In
the refinement calculus, monotonic predicate transformers are used to
model specifications for (imperative) programs. Together with a natural
notion of simulation, they form a category enjoying many algebraic
properties.
We build on this structure to make predicate transformers into a
denotational model of full linear logic: all the logical
constructions have a natural interpretation in terms of predicate
transformers (i.e., in terms of specifications). We then
interpret proofs of a formula by a safety property for the corresponding
specification.
 Neil Immerman, Alex Rabinovich, Tom Reps, Mooly
Sagiv, and Greta Yorsh
 The Boundary Between Decidability and Undecidability for Transitive
Closure Logics

To reason effectively about programs, it is important to have some
version of a transitiveclosure operator so that we can describe such
notions as the set of nodes reachable from a program's variables. On
the other hand, with a few notable exceptions, adding transitive closure
to even very tame logics makes them undecidable. In this paper, we
explore the boundary between decidability and undecidability for
transitiveclosure logics. Rabin proved that the monadic secondorder
theory of trees is decidable, although the complexity of the decision
procedure is not elementary. If we go beyond trees, however,
undecidability comes immediately. We have identified a rather weak
language called EA(TC+[E]) that goes beyond trees, includes a version of
transitive closure, and is decidable. We show that satisfiability of
EA(TC+[E]) is NEXPTIME complete. We furthermore show that essentially
any reasonable extension of EA(TC+[E]) is undecidable. Our main
contribution is to demonstrate these sharp divisions between decidable
and undecidable. We also compare the complexity and expressibility of
EA(TC+[E]) with related decidable languages including MSO(trees) and
guarded fixed point logics. We mention possible applications to systems
some of us are building that use decidable logics to reason about
programs.
 Yukiyoshi Kameyama
 Axioms for Delimited Continuations in the CPS Hierarchy

A CPS translation is a syntactic translation of programs, which is
useful for describing their operational behavior. By iterating the
standard callbyvalue CPS translation, Danvy and Filinski discovered
the CPS hierarchy and proposed a family of control operators, shift and
reset, that make it possible to capture successive delimited
continuations in a CPS hierarchy. Although shift and reset have found
their applications in several areas such as partial evaluation, most
studies in the literature have been devoted to the base level of the
hierarchy, namely, to level1 shift and reset. In this article, we
investigate the whole family of shift and reset. We give a simple
calculus with leveln shift and leveln reset for an
arbitrary n>0. We
then give a set of equational axioms for them, and prove that these
axioms are sound and complete with respect to the CPS translation. The
resulting set of axioms is concise and a natural extension of those for
level1 shift and reset.
 Margarita Korovina and Nicolai Vorobjov
 Pfaffian Hybrid Systems

It is well known that in an ominimal hybrid system the continuous and
discrete components can be separated, and therefore the problem of
finite bisimulation reduces to the same problem for a transition system
associated with a continuous dynamical system. It was recently proved by
several authors that under certain natural assumptions such finite
bisimulation exists. In the paper we consider ominimal systems defined
by Pfaffian functions, either implicitly (via triangular systems of
ordinary differential equations) or explicitly (by means of
semiPfaffian maps). We give explicit upper bounds on the sizes of
bisimulations as functions of formats of initial dynamical systems. We
also suggest an algorithm with an elementary (doublyexponential) upper
complexity bound for computing finite bisimulations of these systems.
 Christopher Lynch
 Unsound Theorem Proving

We discuss the benefits of complete unsound inference procedures for
efficient methods of disproof. We give a framework for converting a
sound and complete saturationbased inference procedure into successive
unsound and complete procedures, that serve as successive approximations
to the theory. The idea is to successively add new statements in such a
way that the inference procedure will halt. Then the satisfiability is
evaluated over a stronger theory. This gives an overapproximation to
the given theory. We show how to successively compute better
overapproximations. Similarly, a sound and incomplete theorem prover
will give an underapproximation. In our framework, we successively
compute better over and underapproximations in this way. We illustrate
this framework with KnuthBendix Completion, and show that in some
theories this method becomes a decision procedure. Then we illustrate
the framework with a new method for the (nonground) word problem, based
on Congruence Closure. We show a class where this becomes a decision
procedure. Also, we show that this new inference system is interesting
in its own right. Given a particular goal, in many cases we can halt
the procedure at some point and say that all the equations for solving
the goal have been generated already. This is generally not possible in
KnuthBendix Completion.
 Patrick Maier
 Intuitionistic LTL and a New Characterization of Safety and
Liveness
 Classical lineartime temporal logic (LTL) is capable of specifying
of and reasoning about infinite behaviors only. While this is appropriate
for specifying nonterminating reactive systems, there are situations
(e.g., assumeguarantee reasoning, runtime verification) when it is
desirable to be able to reason about finite and infinite behaviors. We
propose an interpretation of the operators of LTL on finite and infinite
behaviors, which defines an intuitionistic temporal logic (ILTL).
We compare the expressive power of LTL and ILTL. We demonstrate that
ILTL is suitable for assumeguarantee reasoning and for expressing
properties that relate finite and infinite behaviors. In particular,
ILTL admits an elegant logical characterization of safety and liveness
properties.
 George Metcalfe, Nicola Olivetti,
and Dov Gabbay
 GoalDirected Methods for Lukasiewicz Logic
 In this paper we present goaldirected deduction methods for
Lukasiewicz infinitevalued logic L, giving logic programming style
algorithms which both have a logical interpretation, and provide a
suitable basis for implementation. We begin by considering a basic version
with connections to calculi for other logics, then make refinements to
obtain greater efficiency and termination properties, and to treat further
connectives and truth constants. We finish by considering applications
of these algorithms to fuzzy logic programming.
 David Richerby
 Logical Characterizations of PSPACE

We present two, quite different, logical characterizations of the
computational complexity class PSPACE on unordered, finite relational
structures. The first of these, the closure of secondorder logic under
the formation of partial fixed points is wellknown in the folklore but
does not seem to be in the literature. The second, the closure of
firstorder logic under taking partial fixed points and under an
operator for nondeterministic choice, is novel. We also present
syntactic normal forms for the two logics and compare the second with
other choicebased fixedpoint logics found in the literature.
 Philipp Rohde
 Moving in a Crumbling Network: The Balanced Case
 In
this paper we continue the study of “sabotage modal logic” SML which
was suggested by van Benthem. In this logic one describes the
progression along edges of a transition graph in alternation with moves
of a saboteur who can delete edges. A drawback of the known results on
SML is the asymmetry of the two modalities of “moving” and
“deleting”.
Movements are local, whereas there is a global choice for edge deletion.
To balance the situation and to obtain a more realistic model for
traffic and network problems, we require that also the sabotage moves
(edge deletions) are subject to a locality condition. We show that the
new logic, called path sabotage logic PSL, already has the same
complexities as SML (model checking, satisfiability) and that it lacks
the finite model property. The main effort is finding a pruned form of
SMLmodels that can be enforced within PSL and giving appropriate
reductions from SML to PSL.
 Pawel Rychlikowski and Tomasz Truderung
 Set Constraints on Regular Terms

Set constraints are a useful formalism for verifying properties of
programs. Usually, they are interpreted over the universe of finite
terms. However, some logic languages allow infinite regular terms, so
it seems natural to consider set constraints over this domain. In the
paper we show that the satisfiability problem of set constraints over
regular terms is undecidable. We also show that, if each function symbol
has the arity at most 1, then this problem is EXPSPACEcomplete.
 Ulrich Schöpp and Ian Stark
 A Dependent Type Theory with Names and Binding
 We consider the problem of providing formal support for working with
abstract syntax involving variable binders. Gabbay and Pitts have shown
in their work on FraenkelMostowski (FM) set theory how to address this
through firstclass names: in this paper we present a dependent type theory
for programming and reasoning with such names. Our development is based
on a categorical axiomatization of names, with freshness as its central
notion. An associated adjunction captures constructions known from FM
theory: the freshness quantifier, namebinding, and unique choice of
fresh names. We show that the Schanuel topos — the category underlying
FM set theory — is an instance of this axiomatization. Working from
the categorical structure, we define a dependent type theory which it
models. This uses bunches to integrate the monoidal structure corresponding
to freshness, from which we define novel multiplicative dependent products
and sums, as well as a propositionsastypes generalization of the freshness
quantifier.
 Lutz Schröder
 The Logic of the Partial λCalculus With Equality
 We investigate the logical aspects of the partial lambdacalculus with
equality, exploiting an equivalence between partial lambdatheories and
partial cartesian closed categories (pcccs) established here. The partial
lambdacalculus with equality provides a fullblown intuitionistic higher
order logic, which in a precise sense turns out to be almost the logic of
toposes, the distinctive feature of the latter being unique choice. We
prove in a linguistic fashion that the fundamental theorem of toposes
generalizes to pcccs with equality; type theoretically, this means that
the partial lambdacalculus with equality encompasses a MartinLöfstyle
dependent type theory. This work forms part of the semantical foundations
for the higher order algebraic specification language HasCASL.
 Aleksy Schubert
 On the Building of Affine Retractions
 A simple
type σ is retractable to a simple type τ if there are
two terms C:σ→τ and D:τ→σ
such that D°C = λx.x
w.r.t. βηequivalence. The paper presents a system which
for given σ, τ derives affine retractability, i.e.,
the above relation with additional restriction that in C and
D every bound variable occurs at most once. A derivation in the
system constructs these terms. What is more, the complexity of building
affine retractions is studied. The problem of affine retractability is
NPcomplete even for the class of types over single type atom and having
limited functional order. A polynomial algorithm for types of orders
less than 3 is also presented.
 Alan Skelley
 A ThirdOrder Bounded Arithmetic Theory for PSPACE

We present a novel thirdorder theory W_{1}^{1}
of bounded arithmetic suitable for reasoning about PSPACE functions.
This theory has the advantages of avoiding the smash function symbol and
is otherwise much simpler than previous PSPACE theories. As an example
we outline a proof in W_{1}^{1}
that from any configuration in the game of
Hex, at least one player has a winning strategy. We then exhibit a
translation of theorems of W_{1}^{1} into
families of propositional tautologies with polynomialsize proofs in
BPLK (a recent propositional proof system for PSPACE and an alternative
to G). This translation is clearer and more natural in several respects
than the analogous ones for previous PSPACE theories.
 Lutz Straßburger and
François Lamarche
 On Proof Nets for Multiplicative Linear Logic with Units
 In this paper we present a theory of proof nets for
multiplicative linear logic including the two units. It naturally
extends the wellknown theory of unitfree multiplicative proof nets. A
linking is no longer a set of axiom links but a tree in which the axiom
links are subtrees. These trees will be identified according to an
equivalence relation based on a simple form of graph rewriting. We show
the standard results of sequentialization and strong normalization of
cut elimination. Furthermore, the identifications enforced on proofs
are such that the proof nets, as they are presented here, form the
arrows of the free (symmetric) *autonomous category.
 Jérôme Vouillon
 Subtyping Union Types
 Subtyping
can be fairly complex for union types, due to interactions
with other types, such as function types. Furthermore,
these interactions turn out to depend on the calculus considered: for
instance, a callbyvalue calculus and a callbyname calculus will have
different possible subtyping rules. In order to abstract
ourselves away from this dependence, we consider a fairly large class of
calculi. This allows us to find a subtyping relation which is both
robust (it is sound for all calculi) and precise (it is complete with
respect to the class of calculi).
 Tjark Weber
 Towards Mechanized Program Verification with Separation
Logic
 Using separation logic, this paper presents three Hoare logics
(corresponding to different notions of correctness) for the simple While
language extended with commands for heap access and modification.
Properties of separating conjunction and separating implication
are mechanically verified and used to prove soundness and relative
completeness of all three Hoare logics. The whole development,
including a formal proof of the Frame Rule, is carried out in the
theorem prover Isabelle/HOL.
A BibTeX database is available as a separate
file.
An online
version of the conference
proceedings is available at Springer
www site.
Last modified:
Sep 14, 2004, 13:16