[Home] [Programme] [Timetable] [Venue] [Registration Accepted papers
  1. 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 fixed-point unfolding. Two solutions of this problem are proposed: The first one is a system with equi-recursive non-strictly positive type operators of arbitrary finite kinds, where fixed-point 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.
  2. Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal Zilio, and Line Jakubiec
    A Functional Scenario for Bytecode Verification of Resource Bounds
    We consider a scenario where (functional) programs in pre-compiled 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 first-order 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 quasi-interpretations and of termination verification based on lexicographic path orders leads to an explicit bound on the space required for the execution.
  3. Marcelo Arenas, Pablo Barceló, and Leonid Libkin
    Game-based 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 game-based notions of locality can often be applied when traditional isomorphism-based locality cannot. Our goal is to study game-based 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 game-based notions of locality.
  4. 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.
  5. Mikolaj Bojanczyk
    A Bounding Quantifier
    The logic MSOL+B is defined, by extending monadic second-order 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 B-free formula; and formulas built from B-free formulas by nesting B, ∃, ∨ and ∧.
  6. Krishnendu Chatterjee, Rupak Majumdar, and Marcin Jurdzinski
    On Nash Equilibria in Stochastic Games
    We study infinite stochastic games played by n-players 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 Ri 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 n-player 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 (v1,...,vn), it is NP-complete to determine if there exists a pure, memoryless ε-Nash equilibrium where each player gets payoff at least vi. Our techniques for general nonzero sum games also yield NP ∩ coNP ε-approximation algorithms for zero-sum reachability games, improving the previously known EXPTIME bound. We study the important subclass of n-player perfect-information or turn-based probabilistic games, where at each state at most one player has a nontrivial choice of moves. For turn-based probabilistic games, we show the existence of ε-Nash equilibria in pure strategies for games where the objective of player i is a Borel set Bi 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.
  7. 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 T-norm based Logic SMTL.
  8. Andrés Cordón-Franco, Alejandro Fernández-Margarit, and F. Félix Lara-Martí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.
  9. Jeremy E. Dawson and Rajeev Goré
    A General Theorem on Termination of Rewriting
    We re-express our theorem on the strong-normalisation of display calculi as a theorem about the well-foundedness of a certain ordering on first-order terms, thereby allowing us to prove the termination of systems of rewrite rules. We first show how to use our theorem to prove the well-foundedness 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 Knuth-Bendix ordering and of dependency pairs.
  10. Philippe de Groote and Sylvain Salvati
    Higher-order Matching in the Linear λ-calculus with Pairing
    We prove that higher-order matching in the linear λ-calculus with pairing is decidable. We also establish its NP-completeness under the assumption that the right-hand side of the equation to be solved is given in normal form.
  11. 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.
  12. E. Allen Emerson and Vineet Kahlon
    Parameterized Model Checking of Ring-based 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 stuttering-insensitive 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.
  13. Harald Ganzinger and Konstantin Korovin
    Integrating Equational Reasoning into Instantiation-based Theorem Proving
    In this paper we present a method for integrating equational reasoning into instantiation-based 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.
  14. Roberto Giacobazzi and Isabella Mastroeni
    Proving Abstract Non-Interference
    In this paper we introduce a compositional proof-system for certifying abstract non-interference in programming languages. Certifying abstract non-interference 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 proof-system specifies how these assertions can be composed in a syntax-directed á la Hoare deduction of secrecy. We prove that the proof-system is sound relatively to the standard semantics of an imperative programming language with non-deterministic choice. This provides a sound proof-system for both certifying secrecy in language-based security and deriving attackers which do not violate secrecy inductively on program's syntax.
  15. Hugo Gimbert
    Parity and Exploration Games on Infinite Graphs
    This paper examines two players' turn-based perfect-information 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.
  16. Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, and Yu Zhang
    Complete Lax Logical Relations for Cryptographic Lambda-Calculi
    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 lambda-calculus. We clarify Sumii and Pierce's approach, using a cryptographic version of Moggi's monadic lambda-calculus 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 (non-lax) at monad types. We show that they are sound and complete for contextual equivalence at all types.
  17. 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.
  18. 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 transitive-closure 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 transitive-closure logics. Rabin proved that the monadic second-order 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.
  19. 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 call-by-value 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 level-1 shift and reset. In this article, we investigate the whole family of shift and reset. We give a simple calculus with level-n shift and level-n 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 level-1 shift and reset.
  20. Margarita Korovina and Nicolai Vorobjov
    Pfaffian Hybrid Systems
    It is well known that in an o-minimal 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 o-minimal systems defined by Pfaffian functions, either implicitly (via triangular systems of ordinary differential equations) or explicitly (by means of semi-Pfaffian 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 (doubly-exponential) upper complexity bound for computing finite bisimulations of these systems.
  21. 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 saturation-based 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 over-approximation to the given theory. We show how to successively compute better over-approximations. Similarly, a sound and incomplete theorem prover will give an under-approximation. In our framework, we successively compute better over and under-approximations in this way. We illustrate this framework with Knuth-Bendix 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 Knuth-Bendix Completion.
  22. Patrick Maier
    Intuitionistic LTL and a New Characterization of Safety and Liveness
    Classical linear-time temporal logic (LTL) is capable of specifying of and reasoning about infinite behaviors only. While this is appropriate for specifying non-terminating reactive systems, there are situations (e.g., assume-guarantee reasoning, run-time 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 assume-guarantee reasoning and for expressing properties that relate finite and infinite behaviors. In particular, ILTL admits an elegant logical characterization of safety and liveness properties.
  23. George Metcalfe, Nicola Olivetti, and Dov Gabbay
    Goal-Directed Methods for Lukasiewicz Logic
    In this paper we present goal-directed deduction methods for Lukasiewicz infinite-valued 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.
  24. 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 second-order logic under the formation of partial fixed points is well-known in the folklore but does not seem to be in the literature. The second, the closure of first-order 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 choice-based fixed-point logics found in the literature.
  25. 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 SML-models that can be enforced within PSL and giving appropriate reductions from SML to PSL.
  26. 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 EXPSPACE-complete.
  27. 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 Fraenkel-Mostowski (FM) set theory how to address this through first-class 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, name-binding, 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 propositions-as-types generalization of the freshness quantifier.
  28. Lutz Schröder
    The Logic of the Partial λ-Calculus With Equality
    We investigate the logical aspects of the partial lambda-calculus with equality, exploiting an equivalence between partial lambda-theories and partial cartesian closed categories (pcccs) established here. The partial lambda-calculus with equality provides a full-blown 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 lambda-calculus with equality encompasses a Martin-Löf-style dependent type theory. This work forms part of the semantical foundations for the higher order algebraic specification language HasCASL.
  29. 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 NP-complete 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.
  30. Alan Skelley
    A Third-Order Bounded Arithmetic Theory for PSPACE
    We present a novel third-order theory W11 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 W11 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 W11 into families of propositional tautologies with polynomial-size 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.
  31. 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 well-known theory of unit-free 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.
  32. 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 call-by-value calculus and a call-by-name 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).
  33. 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 on-line version of the conference proceedings is available at Springer www site.

Last modified: Sep 14, 2004, 13:16