LICS on Monday, July 12th

09:00‑10:00 Invited Lecture
Chair: Rajev Alur
Location: AT LT4
09:00 Martin Abadi (Microsoft Research and UCSC)
The Fine print of Security

Simple views of systems are often convenient in their design and analysis. However, attackers may attempt to exploit any oversimplification. For security, it is therefore useful to understand the value and the limitations of simplistic models. Computational-soundness theorems, which are the main subject of this lecture, can sometimes shed light on this question.<br/> We discuss them first in the context of security protocols. There, two distinct, rigorous views of cryptography have developed over the years. One of the views relies on a simple but powerful symbolic approach; the other, on a detailed computational model that considers issues of probability and complexity. In the last decade, however, we have made sub- stantial progress in bridging the gap between these views. This progress, of which a paper with Phil Rogaway was one of the early steps, is due to many researchers. By now, this line of work provides computational justifications for formal treatments of cryptographic operations and security protocols, and also explores hybrid approaches.<br/> Similar ideas can apply in the domain of software protection, although they are less mature in this domain. Specifically, we can relate high-level security guarantees, of the kind offered by programming-language semantics, with lower-level properties of implementations. Layout randomization, one popular and effective implementation technique, again brings up issues of probability and complexity. The lecture introduces some recent work with Gordon Plotkin on this topic.<br/>

10:30‑12:30 Semantics
Chair: Martin Abadi
Location: AT LT4
10:30 Joerg Endrullis, Dimitri Hendriks and Jan Willem Klop
Modular Construction of Fixed Point Combinators and Clocked Boehm Trees

Fixed point combinators (and their generalization: looping combinators) are classic notions belonging to the heart of lambda calculus and logic. We start with an exploration of the structure of fixed point combinators (fpc's), vastly generalizing the well-known fact that if Y is an fpc, Y(SI) is again an fpc, generating the Boehm sequence of fpc's. Via a detour in the infinitary lambda calculus we devise infinitely many other generation schema's for fpc's. In this way we find schemes and building blocks to construct new fpc's in a modular way. This construction seems to be free, in the sense that no identifications arise; in other words, that fpc's obey a prime factorization property. For our class of new fpc's this holds; in general the prime factorization is an open question, first raised (in a particular simple version) by Statman.

Having created a plethora of new fixed point combinators, the task is to prove that they are indeed new. That is, we have to prove their beta-inconvertibility. Known techniques via Boehm Trees do not apply, as observed by Scott, asking for a proof that BY is not beta-convertible with BYS, because all fpc's have the same BT. To this end, we give a new Boehm-Tree based semantics of lambda calculus by means of clocked Boehm Trees, with annotations that convey information of the tempo in which the data in the Boehm Tree are produced. Boehm Trees are thus enriched with an intrinsic clock behaviour. Analyzing this clock behaviour leads to a refined discrimination method for lambda terms. The corresponding equality is strictly intermediate between beta-convertibility and BT-equality, the equality in the classical models of lambda calculus. An analogous approach can be obtained for Levi-Longo and Berarducci trees.

11:00 Christopher Broadbent, Arnaud Carayol, C.-H. Luke Ong and Olivier Serre
Recursion Schemes and Logical Reflection

Let R be a class of generators of node-labelled infinite trees, and L be a logical language for describing correctness properties of these trees. Given r in R and phi in L, we say that r_phi is a phi-reflection of r just if (i) r and r_phi generate the same underlying tree, and (ii) suppose a node u of the tree t(r) generated by r has label f, then the label of the node u of t(r_phi) is f* if u in t(r) satisfies phi; it is f otherwise. Thus if t(r) is the computation tree of a program r, we may regard r_phi as a transform of r that can internally observe its behaviour against a specification phi. We say that R is (constructively) reflective w.r.t. L just if there is an algorithm that transforms a given pair (r,phi) to r_phi.

In this paper, we prove that higher-order recursion schemes are reflective w.r.t. both modal mu-calculus and monadic second order (MSO) logic. To obtain this result, we give the first characterisation of the winning regions of parity games over the transition graphs of collapsible pushdown automata (CPDA): they are regular sets defined by a new class of automata. (Order-n recursion schemes are equi-expressive with order-n CPDA for generating trees.) As a corollary, we show that these schemes are closed under the operation of MSO-interpretation followed by tree unfolding a la Caucal.

11:30 James Brotherston and Max Kanovich, Dominique Larchey-Wendling and Didier Galmiche.
Undecidability of Boolean BI, and of propositional separation logic and its neighbours
12:00 Paul-André Melliès
Segal condition meets computational effects

Lawvere observed in his PhD thesis that every finitary monad T on the category of sets is described by an algebraic theory whose n-ary operations are precisely the elements of the free algebra Tn generated by n elements. This canonical presentation of the monad is fundamental, and offers a precious guide in the search for a concrete presentation by generators and relations. Hence, much work has been devoted to extend these ideas to situations of computational interest, like enriched categories, or algebraic structures admitting operations of infinite arity. In this paper, we clarify the conceptual nature of these extended Lawvere theories, by uncovering the change-of-arity mechanisms which underlie them. To that purpose, we start from the Segal condition recently formulated and established by Weber for a general notion of monad with arity. Our first contribution is to establish the Segal condition by a nice and conceptual argument based on the discovery of a Beck-Chevalley property satisfied by the change-of-arity operations. Our second contribution is to define an abstract notion of Lawvere theory with arity, which extends to every category and every arity the traditional correspondence between Lawvere theories and finitary monads on Set. We explain how this abstract approach to Lawvere theories clarifies the notion of enriched Lawvere A-theory recently introduced by Nishizawa and Power. We also illustrate the concrete benefits of Lawvere's ideas by describing how the elegant and intuitive presentation of the state monad formulated by Plotkin and Power is ultimately validated by a rewriting property on sequences of updates and lookups.

14:00‑15:00 Finite Model Theory
Chair: Stephan Kreutzer
Location: AT LT4
14:00 Dietrich Kuske, Jiamou Liu and Markus Lohrey
The Isomorphism Problem On Classes of Automatic Structures

Automatic structures are finitely presented structures where the universe and all relations can be recognized by finite automata. It is known that the isomorphism problem for automatic structures is complete for $\Sigma^1_1$; the first existential level of the analytical hierarchy. Several new results on isomorphism problems for automatic structures are shown in this paper: (i) The isomorphism problem for automatic equivalence relations is complete for $\Pi^0_1$ (first universal level of the arithmetical hierarchy). (ii) The isomorphism problem for automatic trees of height $n \geq 2$ is $\Pi^0_{2n-3}$-complete. (iii) The isomorphism problem for automatic linear orders is not arithmetical. This solves some open questions of Khoussainov, Rubin, and Stephan.

14:30 Yuguo He
On the strictness of the first-order quantifier structure hierarchy over finite structures

Separating the expressibility power of different logics or fragments of logics is among the major interests of finite model theory, which is closely related to the separating of complexity classes. In 1996, Gr\"adel and McColm proposed a conjecture about separating expressibility classes based on prefix. If the conjecture is true, these classes form a strict hierarchy, which can be called first-order prefix hierarchy. In 1998, Rosen proved that this conjecture holds over infinite structures. However, the conjecture remains open over finite structures because most classical model-theoretic techniques fail to produce finite structures. In this paper, we give a proof for Gr\"adel and McColm's conjecture, and generalize it to the separating of expressibility classes based on quantifier structures, all over finite structures.

15:30‑17:00 Finite Model Theory
Chair: Yijia Chen
Location: AT LT4
15:30 Martin Grohe
Fixed-Point Definability and Polynomial Time on Graphs with Excluded Minors

We prove that fixed-point logic with counting captures polynomial time on all classes of graphs with excluded minors. That is, for every class C of graphs such that some graph H is not a minor of any graph in C, a property P of graphs in C is decidable in polynomial time if and only if it is definable in fixed-point logic with counting. Furthermore, we prove that for every class C of graphs with excluded minors there is a k such that the k-dimensional Weisfeiler-Leman algorithm decides isomorphism of graphs in C in polynomial time. The Weisfeiler-Leman algorithm is a combinatorial algorithm for testing isomorphism. It generalises the basic colour refinement algorithm and is much simpler than the known group-theoretic algorithms for deciding isomorphism of graphs with excluded minors.

The main technical theorem behind these two results is a "definable structure theorem" for classes of graphs with excluded minors. It states that graphs with excluded minors can be decomposed into pieces arranged in a treelike structure, together with a linear order of each of the pieces. Furthermore, the decomposition and the linear orders on the pieces are definable in fixed-point logic (without counting).

16:00 Stephan Kreutzer and Siamak Tazari
Lower Bounds for the Complexity of Monadic Second-Order Logic

Courcelle's famous theorem from 1990 states that any property of graphs definable in monadic second-order logic (MSO_2) can be decided in linear time on any class of graphs of bounded tree-width, or in other words, MSO_2 is fixed-parameter tractable in linear time on any such class of graphs. From a logical perspective, Courcelle's theorem establishes a sufficient condition, or an upper bound, for tractability of MSO_2-model checking.

Whereas such upper bounds on the complexity of logics have received significant attention in the literature, almost nothing is known about corresponding lower bounds. In this paper we establish a strong lower bound for the complexity of monadic second-order logic. In particular, we show that if C is any class of graphs which is closed under taking sub-graphs and whose tree-width is not bounded by a poly-logarithmic function (in fact, log^c n for some small c suffices) then MSO_2-model checking is intractable on C (under a suitable assumption from complexity theory).

16:30 Bastian Laubner
Capturing Polynomial Time on Interval Graphs

We prove a characterization of all polynomial-time computable queries on the class of interval graphs by sentences of fixed-point logic with counting. More precisely, it is shown that on the class of unordered interval graphs, any query is polynomial-time computable if and only if it is definable in fixed-point logic with counting. This result is one of the first establishing the capturing of polynomial time on a graph class which is defined by forbidden induced subgraphs. For this, we define a canonical form of interval graphs using a type of modular decomposition, which is different from the method of tree decomposition that is used in most known capturing results for other graph classes, specifically those defined by forbidden minors. The method might also be of independent interest for its conceptual simplicity. Furthermore, it is shown that no logic containing first-order logic can capture polynomial time on the classes of chordal graphs or incomparability graphs unless it captures polynomial time on the class of all graphs.

17:15‑18:15 Logics
Chair: Dan Ghica
Location: AT LT4
17:15 Patricia Johann, Alex Simpson and Janis Voigtländer
A Generic Operational Metatheory for Algebraic Effects

We provide a syntactic analysis of contextual preorder and equivalence for a polymorphic programming language with effects. Our approach applies uniformly to arbitrary {algebraic effects}, and thus incorporates, as instances: errors, input/output, global state, nondeterminism, probabilistic choice, and combinations thereof. Our approach is to extend Plotkin and Power's structural operational semantics for algebraic effects (FoSSaCS 2001) with a primitive ``basic preorder'' on ground type computation trees. The basic preorder is used to derive notions of contextual preorder and equivalence on program terms. Under mild assumptions on this relation, we prove fundamental properties of contextual preorder (hence equivalence) including extensionality properties, a characterization via applicative contexts, and machinery for reasoning about polymorphism using relational parametricity.

17:45 Noam Zeilberger
Polarity and the logic of delimited continuations

Classical polarized logic is the logic of continuation-passing style, and in that sense provides a language for reflecting evaluation order at the level of types. The main limitations of this logic are the limitations of CPS: that continuations cannot be composed, and that programs must be fully sequentialized. In response to the limitations of classical continuation-passing, delimited continuations were invented. That suggests the question: what is the logic of delimited continuations?

In this paper, we give a simple account of delimited continuations through a natural generalization of classical polarized logic. This amounts to breaking the perfect symmetry between positive and negative polarity in the following way: answer types are positive. Despite this asymmetry, we retain all of the classical polarized connectives (e.g., $\Par$), and can explain ``intuitionistic polarity'' (in systems like call-by-push-value, etc.) as a restriction on the use of connectives, i.e., as a logical fragment. Our analysis simplifies and generalizes existing accounts of delimited control operators, while giving us a rich logical language through which to approach the combination of delimited control with other forms of effects.