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. I present highlights from a formalized development of do- main theory in the theorem prover Coq. This is the first development of domain theory that is effective, formalized and that supports all the usual constructions on domains. In particular, I develop constructive models of both the unpointed profinite and the pointed profinite domains. tandard constructions (e.g., products, sums, the function space, and powerdomains) are all developed. In addition, I build the machinery necessary to compute solutions to recursive domain equations.

ABSTRACT. We prove completeness and decidability results for the temporal logic CTL in Coq/Ssreflect. Our basic result is a constructive proof that for every formula one can obtain either a finite model satisfying the formula or a proof in a Hilbert system certifying the unsatisfiability of the formula. The proof is based on a history-augmented tableau system obtained as the dual of Brünnler and Lange's cut-free sequent calculus for CTL. We prove the completeness of the tableau system and give a translation of tableau refutations into Hilbert refutations. Decidability of CTL and completeness of the Hilbert system follow as corollaries.

ABSTRACT. Universes are used in Type Theory to ensure consistency by checking that definitions are well-stratified according to a certain hierarchy. In the case of the Coq proof assistant, based on the predicative Calculus of Inductive Constructions (pCIC), this hierachy is built from an impredicative sort Prop and an infinite number of predicative Type(i) universes. A cumulativity relation represents the inclusion order of universes in the core theory. Originaly, universes were thought to be floating levels, and definitions implicitely constrained these levels in a consistent manner. This works well for most theories, however the globality of the levels and the constraints precluded generic constructions on universes that could work at different levels. Universe polymorphism extends this setup by adding local bindings of universes and constraints, supporting generic definitions over universes, reusable at different levels. This provides the same kind of code reuse facilities as ML-style parametric polymorphism. However, the structure and hierarchy of universes is more complex than bare polymorphic type variables. In this paper, we introduce a conservative extension of pCIC supporting universe polymorphism and treating its whole hierarchy. This new design supports typical ambiguity and implicit polymorphic generalization at the same time, keeping it mostly transparent to the user. Benchmarking the implementation as an extension of the Coq proof assistant on real-world examples gives encouraging results.

ABSTRACT. Current work on computational reflection is single-minded; each reflective procedure is written with a specific application or scope in mind. Composition of these reflective procedures is done by a proof-generating tactic language such as Ltac. This composition, however, comes at the cost of both larger proof terms and redundant preprocessing. In this work, we propose a methodology for writing composable reflective procedures that solve many small tasks in a single invocation. The key technical insights are techniques for reasoning semantically about extensible syntax in intensional type theory. We also consider how users can customize the behavior of reflective procedures by packaging additional information and passing it to them. This mimicks Coq's usual support for hint databases with only slightly more user effort. We evaluate our techniques in the context of imperative program verification.

ABSTRACT. We discuss the difference between a formal semantics of the C standard, and a formal semantics of an implementation of C that satisfies the C standard. In this context we extend the CompCert semantics with end-of-array pointers and the possibility to byte-wise copy objects. This is a first and necessary step towards proving that the CompCert semantics satisfies the formal version of the C standard that is being developed in the Formalin project in Nijmegen.

ABSTRACT. Completion is one of the most studied techniques in term rewriting. We present a new proof of the correctness of abstract completion that is based on peak decreasingness, a special case of decreasing diagrams. Peak decreasingness replaces Newman's Lemma and allows us to avoid proof orders in the correctness proof of completion. As a result, our proof is simpler than the one presented in textbooks, which is confirmed by our Isabelle/HOL formalization. Furthermore, we show that critical pair criteria are easily incorporated in our setting.

ABSTRACT. We propose a revised constructive specification and a certified entangled linked implementation of combinatorial hypermaps using a general notion of orbit. Combinatorial hypermaps help to prove theorems in algebraic topology and to develop algorithms in computational geometry. Orbits unify the presentation at conceptual and concrete levels and reduce the proof effort. All the development is formalized and verified in the Coq proof assistant. The implementation is easily proved observationally equivalent to the specification and translated in C language. Our method is transferable to a great class of algebraic specifications implemented into complex data structures with entangled or nested linear, circular or symmetric linked lists, and pointer arrays.

ABSTRACT. Reducing the distance between informal and formal proofs in interactive theorem proving is a long-standing matter. An approach to this general topic is to increase automation in theorem provers: indeed, automation turns many small formal steps into one big step. Inspite of the usual automation methods, there are still many situations where the user has to provide some information manually, whereas this information could be derived from the context. In this paper, we characterize some very common use cases where such situations happen, and identify some general patterns behind them. We then provide solutions to deal with these situations automatically, which we implemented as HOL Light and HOL4 tactics. We find these tactics to be extremely useful in practice, not only for their automation but also for the feedback that they provide to the user.

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).