View: session overviewtalk overviewside by side with other conferences
08:45  FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change? SPEAKER: Sweitze Roffel 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 shortterm research; the tension between the ideal of open access and the reality of readerpay 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. 
10:45  HyperAckermannian Bounds for Pushdown Vector Addition Systems SPEAKER: Grégoire Sutre 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 wellstructured pushdown systems. We show that the worstcase running time of this algorithm is hyperAckermannian for pushdown vector addition systems. For the upper bound, we introduce the notion of bad nested words over a wellquasiordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyperAckermannian 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 (hyperAckermannian). 
11:15  Preservation and Decomposition Theorems for Bounded Degree Structures SPEAKER: Lucas Heimberg ABSTRACT. We provide elementary algorithms for two preservation theorems for firstorder 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 existentialpositive (existential) FOsentence can be constructed in 4fold (6fold) exponential time. For FOsentences, the algorithm has 4fold (5fold) exponential time complexity. This is complemented by lower bounds showing that for FOsentences a 3fold exponential blowup of the computed existentialpositive (existential) sentence is unavoidable. Furthermore, we show that for an input FOformula, a C_{d}equivalent FefermanVaught decomposition can be computed in 3fold exponential time. We also provide a matching lower bound. 
11:45  On the Succinctness of Query Rewriting over OWL 2 QL Ontologies with Bounded Chase SPEAKER: Roman Kontchakov ABSTRACT. We investigate the size of firstorder 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 polynomialsize nonrecursive datalog rewritings; treeshaped 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 firstorder rewritings are superpolynomial unless NP \subseteq P/poly. We also analyse rewritings of treeshaped queries over arbitrary ontologies and observe that the query entailment problem for such queries is fixedparameter tractable. 
12:15  MSO Queries on Trees: Enumerating Answers under Updates SPEAKER: Katja Losemann ABSTRACT. We investigate efficient view maintenance for MSOdefinable queries over trees or, more precisely, efficiently enumerating answers of MSOdefinable 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. 
10:45  Transition systems over games SPEAKER: Paul Blain Levy 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.

11:15  Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects SPEAKER: unknown ABSTRACT. Girard's Geometry of Interaction (GoI) is interactionbased 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 statebased machines has been worked out by Mackie, Ghica and others. In this paper, we take Abramsky's idea of resumptionbased 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. 
11:45  Compositional HigherOrder Model Checking via OmegaRegular Games over Boehm Trees SPEAKER: unknown ABSTRACT. We introduce typechecking games, which are omegaregular games over Boehm trees, determined by a type of the KobayashiOng intersection type system. These games are a highertype 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 typechecking 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, typechecking games give the first compositional analysis of higherorder model checking, or the model checking of trees generated by recursion schemes. We study a highertype analogue of higher order model checking, namely, the problem to decide the winner of a typechecking game over the Boehm tree generated by a lambdaYterm. 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 typechecking games, which is a cartesian closed category equipped with parametric monad and comonad that themselves form a parametrised adjunction. 
12:15  On the Hoare Theory of Monadic Recursion Schemes SPEAKER: Konstantinos Mamouras 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 nonelementary. 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 Hoarestyle 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. 
14:30  Decidability of Weak Logics with Deterministic Transitive Closure SPEAKER: Filip Mazowiecki 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 twovariable fragment of firstorder 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 \ExpSpacecomplete. This contrasts with the undecidability of twovariable logic with the deterministic transitive closures of several binary relations, known before. We also consider the class of universal firstorder 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. 
15:00  The Complexity of Admissibility in OmegaRegular Games SPEAKER: Romain Brenguier ABSTRACT. Iterated admissibility is a wellknown and important concept in classical game theory, e.g. to determine behaviors in multiplayer matrix games. As recently shown by Berwanger, this concept can be soundly extended to infinite games played on graphs with omegaregular 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. 
15:30  Pattern Logics and Auxiliary Relations SPEAKER: Leonid Libkin 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 reallife declarative languages. A recent trend is to add a datavalue 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 patternbased 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. 
14:30  KAT + B! SPEAKER: unknown 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. 
15:00  On the characterization of models of H* SPEAKER: Flavien Breuvart ABSTRACT. We give a characterization, with respect a large class of models of untyped lambdacalculus, of those models which are fully abstract for head normalization, i.e., whose equational theory is H*. An extensional Kmodel D is fully abstract if and only if it is hyperimmune, i.e., nonwell founded chains of elements of D cannot be captured by any recursive function. 
15:30  Functional Reactive Types SPEAKER: Alan Jeffrey ABSTRACT. Functional Reactive Programming (FRP) is an approach to streaming data with a pure functional semantics as timeindexed values. In previous work, we showed that Lineartime Temporal Logic (LTL) can be used as a type system for discretetime 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 pasttime 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. 
16:30  Foundations and Technology Competitions Award Ceremony 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:
The following three Boards of Jurors were in charge of choosing the winners:
http://fellowship.logic.at/ 
17:30  FLoC Olympic Games Award Ceremony 1 SPEAKER: Floc Olympic Games 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

18:15  FLoC Closing Week 1 SPEAKER: Helmut Veith 