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. We define the tree automata with height constraints between brothers (TACBB_H). Constraints of equalities and inequalities between heights of siblings that restrict the applicability of the rules are allowed in TACBB_H. These constraints allow to express natural tree languages like complete or balanced (like AVL) trees. We prove decidability of emptiness and finiteness for TACBB_H, and also for a more general class that additionally allows to combine equality and disequality constraints between brothers.

ABSTRACT. The Lambda-mu-calculus is an extension of Parigot’s lambda-mu-calculus, the untyped variant of which is proved by Saurin to satisfy some fundamental properties such as the standardization and the separation theorem. For the untyped Lambda-mu-calculus, Nakazawa and Katsumata gave extensional models, called stream models, which is a simple extension of the lambda models, and in which terms are represented as functions on streams. However, we cannot construct a term model from the Lambda-mu-calculus. This paper introduces an extension of the Lambda-mu-calculus, called Lambda-mu-cons, on which we can construct a term model as a stream model, and its reduction system satisfying confluence, subject reduction, and strong normalization.

ABSTRACT. In this paper we generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first- order term format, thereby facilitating their formal analysis. We show that any transfinite reduction can be faithfully represented as an infinitary proof term, which is unique up to, infinitary, associativity.

Our main use of proof terms is in a definition of permutation equivalence for transfinite reductions, on the basis of permutation equations. This definition involves a variant of equational logic, adapted for dealing with infinite objects.

A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.

ABSTRACT. A connection between lambda calculus and the algebra of near semi-rings is discussed. Among the results is the following completeness theorem. A first-order equation in the language of binary associative distributive algebras is true in all such algebras if and only if the interpretations of the first order terms as lambda terms beta-eta convert to one another. A similar result holds for equations containing free variables.

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