ABSTRACT. Over the last few years, our community has started a collective conversation on several topics related to our publication culture: our emphasis on conference publishing; our large number of specialty conferences; concerns that we have created a culture of hypercritical reviewing, which stifle rather than encourage innovative research; concerns that tenure and promotion practice encourage incremental short-term research; the tension between the ideal of open access and the reality of reader-pay publishing; and the role of social media in scholarly publishing. While computing research has been phenomenally successful, there is a feeling that our publication models are quite often obstacles. Yet, there is no agreement on whether our publication models need to be radically changed or fine tuned, and there is no agreement on how such change may occur. This panel is aimed at furthering the conversation on this topic, with the hope of moving us closer to an agreement.

ABSTRACT. This paper studies the boundedness and termination problems for vector addition systems equipped with one stack. We introduce an algorithm, inspired by the Karp & Miller algorithm, that solves both problems for the larger class of well-structured pushdown systems. We show that the worst-case running time of this algorithm is hyper-Ackermannian for pushdown vector addition systems. For the upper bound, we introduce the notion of bad nested words over a well-quasi-ordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyper-Ackermannian upper bound for the length of bad nested words over vectors of natural numbers. For the lower bound, we exhibit a family of pushdown vector addition systems with finite but large reachability sets (hyper-Ackermannian).

ABSTRACT. We provide elementary algorithms for two preservation theorems for first-order sentences with modulo m counting quantifiers (FO+MOD_m) on the class C_d of all finite structures of degree at most d: For each FO+MOD_m-sentence that is preserved under homomorphisms (extensions) on C_d, a C_d-equivalent existential-positive (existential) FO-sentence can be constructed in 4-fold (6-fold) exponential time. For FO-sentences, the algorithm has 4-fold (5-fold) exponential time complexity. This is complemented by lower bounds showing that for FO-sentences a 3-fold exponential blow-up of the computed existential-positive (existential) sentence is unavoidable.

Furthermore, we show that for an input FO-formula, a C_d-equivalent Feferman-Vaught decomposition can be computed in 3-fold exponential time. We also provide a matching lower bound.

ABSTRACT. We investigate the size of first-order rewritings of conjunctive queries over OWL 2 QL ontologies of depth 1 and 2 by means of hypergraph programs computing Boolean functions. Both positive and negative results are obtained. Conjunctive queries over ontologies of depth 1 have polynomial-size nonrecursive datalog rewritings; tree-shaped queries have quadratic positive existential rewritings; however, in the worst case, positive existential rewritings can only be of superpolynomial size. Positive existential and nonrecursive datalog rewritings of queries over ontologies of depth 2 suffer an exponential blowup in the worst case, while first-order rewritings are superpolynomial unless NP \subseteq P/poly. We also analyse rewritings of tree-shaped queries over arbitrary ontologies and observe that the query entailment problem for such queries is fixed-parameter tractable.

ABSTRACT. We investigate efficient view maintenance for MSO-definable queries over trees or, more precisely, efficiently enumerating answers of MSO-definable queries over words and trees which are subject to local updates. For words we exhibit an algorithm that uses an O(n) preprocessing phase and enumerates answers with O(log n) delay between them. When the word is updated, the algorithm can avoid repeating expensive preprocessing and restart the enumeration phase within O(log n) time. For trees, our algorithm uses O(n) preprocessing time, enumerates answers with O(log^2 n) delay, and can restart enumeration within O(log^2 n) time after receiving an update to the tree. This significantly improves the cost of recomputing the answers of a query from scratch.

ABSTRACT. We describe a framework for game semantics combining operational and denotational accounts.   A game is a bipartite graph of "passive'' and "active'' positions, or a categorical variant with morphisms between positions.

The operational part of the framework is given by a labelled transition system in which each state sits in a particular position of the game.  From a state in a passive position, transitions are labelled with a valid O-move from that position, and take us to a state in the updated position.  Transitions from states in an active position are likewise labelled with a valid P-move, but silent transitions are allowed, which must take us to a state in the same position.

The denotational part is given by a "transfer'' from one game to another, a kind of program that converts moves between the two games, giving an operation on strategies.  The agreement between the two parts is given by a relation called a "stepped bisimulation''.

The framework is illustrated by an example of substitution within a lambda-calculus.

ABSTRACT. Girard's Geometry of Interaction (GoI) is interaction-based semantics of linear logic proofs and, via suitable translations, of functional programs in general. Its mathematical cleanness identifies essential structures in computation; moreover its use as a compilation technique from programs to state-based machines has been worked out by Mackie, Ghica and others. In this paper, we take Abramsky's idea of resumption-based GoI and develop it systematically into a generic framework that accounts for computational effects (nondeterminism, probability, exception, global states, interactive I/O, etc.). The framework is categorical: algebraic operations provide an interface to computational effects (following Plotkin and Power); the framework is built on the categorical axiomatization of GoI by Abramsky, Haghverdi and Scott; and, by use of the coalgebraic formalization of component calculus, the framework describes explicit construction of state machines as interpretations of functional programs. The obtained models are shown to be sound with respect to equations between algebraic operations, as well as to Moggi's standard equations for the computational lambda calculus. The construction is illustrated by concrete examples.

ABSTRACT. We introduce type-checking games, which are omega-regular games over Boehm trees, determined by a type of the Kobayashi-Ong intersection type system. These games are a higher-type extension of parity games over trees, determined by an alternating parity tree automaton. However, in contrast to these games over trees, the "game boards" of our type-checking games are composable, using the composition of Boehm trees. Moreover the winner of a composite game is completely determined by the respective winners of the component games.

To our knowledge, type-checking games give the first compositional analysis of higher-order model checking, or the model checking of trees generated by recursion schemes. We study a higher-type analogue of higher order model checking, namely, the problem to decide the winner of a type-checking game over the Boehm tree generated by a lambda-Y-term. We introduce a new type system and use it to prove that the problem is decidable.

On the semantic side, we develop a novel arena game model for type-checking games, which is a cartesian closed category equipped with parametric monad and comonad that themselves form a parametrised adjunction.

ABSTRACT. The equational theory of monadic recursion schemes is known to be decidable by the result of S\'enizergues on the decidability of the problem of DPDA equivalence. In order to capture some properties of the domain of computation, we augment equations with certain hypotheses. This preserves the decidability of the theory, which we call \emph{simple implicational theory}. The asymptotically fastest algorithm known for deciding the equational theory, and also for deciding the simple implicational theory, has running time that is non-elementary. We therefore consider a restriction of the properties about schemes to check: instead of arbitrary equations $f \equiv g$ between schemes, we focus on propositional Hoare assertions $\{p\}f\{q\}$, where $f$ is a scheme and $p, q$ are tests. Such Hoare assertions have a straightforward encoding as equations. We investigate the \emph{Hoare theory} of monadic recursion schemes, that is, the set of valid implications whose conclusions are Hoare assertions and whose premises are of a certain simple form. We present a sound and complete Hoare-style calculus for this theory. We also show that the Hoare theory can be decided in exponential time, and that it is complete for this class.

ABSTRACT. The deterministic transitive closure operator allows to express many natural properties of a binary relation, including being a linear order, a tree, a forest or a partial function. It makes it a potentially attractive ingredient of computer science formalisms. In this paper we consider the extension of the two-variable fragment of first-order logic by the deterministic transitive closure of a single binary relation, and prove that the satisfiability and finite satisfiability problems for the obtained logic are decidable and \ExpSpace-complete. This contrasts with the undecidability of two-variable logic with the deterministic transitive closures of several binary relations, known before. We also consider the class of universal first-order formulas in prenex form. Its various extensions by deterministic closure operations were earlier considered by other authors, leading to both decidability and undecidability results. We examine this scenario in more details.

ABSTRACT. Iterated admissibility is a well-known and important concept in classical game theory, e.g. to determine behaviors in multi-player matrix games. As recently shown by Berwanger, this concept can be soundly extended to infinite games played on graphs with omega-regular objectives. In this paper, we study the algorithmic properties of this concept for such games. We settle the exact complexity of natural decision problems on the set of strategies that survive iterated elimination of dominated strategies. As a byproduct of our construction, we obtain automata which recognize all the possible outcomes of such strategies.

ABSTRACT. A common theme in the study of logics over finite structures is adding auxiliary predicates to enhance expressiveness and convey additional information. Examples include adding an order or arithmetic for capturing complexity classes, or the power of real-life declarative languages. A recent trend is to add a data-value comparison relation to words, trees, and graphs, for capturing modern data models such as XML and graph databases.

Such additions often result in the loss of good properties of the underlying logic. Our goal is to show that such a loss can be avoided if we use pattern-based logics, standard in XML and graph data querying. The essence of such logics is that auxiliary relations are tested locally with respect to other relations in the structure. These logics are shown to admit strong versions of Hanf and Gaifman locality theorems, which are used to prove a homomorphism preservation theorem, and a decidability result for the satisfiability problem. We discuss applications of these results to pattern logics over data forests, and consequently to querying XML data.

ABSTRACT. Certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests. We show how to axiomatically extend KAT with this feature in the form of mutable tests. The extension is conservative and is formulated as a general commutative coproduct construction. We give several results on deductive completeness and complexity of the system, as well as some examples of its use.

ABSTRACT. We give a characterization, with respect a large class of models of untyped lambda-calculus, of those models which are fully abstract for head normalization, i.e., whose equational theory is H*. An extensional K-model D is fully abstract if and only if it is hyperimmune, i.e., non-well founded chains of elements of D cannot be captured by any recursive function.

ABSTRACT. Functional Reactive Programming (FRP) is an approach to streaming data with a pure functional semantics as time-indexed values. In previous work, we showed that Linear-time Temporal Logic (LTL) can be used as a type system for discrete-time FRP, and that functional reactive primitives perform two roles: as combinators for building streams of data, and as proof rules for constructive LTL. In this paper, we add a third role, by showing that FRP combinators can be used to define streams of types, and that these functional reactive types can be viewed both as a constructive temporal logic, and as the types for functional reactive programs. As an application of functional reactive types, we show that past-time LTL (pLTL) can be extended with FRP to get a logic pLTL+FRP. This logic is expressed as streams of boolean expressions, and so bounded satisfiability of pLTL can be translated to Satisfiability Modulo Theory (SMT). Thus, pLTL+FRP can be used as a constraint language for problems which mix properties of data with temporal properties.

ABSTRACT. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

• Logical Foundations of Mathematics,
• Logical Foundations of Computer Science, and
• Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

• Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
• Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
• Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.

http://fellowship.logic.at/

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• 3rd Confluence Competition (CoCo 2014);
• Configurable SAT Solver Challenge (CSSC 2014);
• Ninth Max-SAT Evaluation (Max-SAT 2014);
• QBF Gallery 2014; and
• SAT Competition 2014 (SAT-COMP 2014).