Tuesday, 8 September 2015
Show all abstracts Proceedings Close all abstracts
9:00  Elham Kashefi  Verification of Quantum Computing  
10:00  Samson Abramsky, Rui Soares Barbosa, Kohei Kishida, Raymond Lal, Shane Mansfield 
Contextuality, Cohomology and Paradox
Show abstract Contextuality is a key feature of quantum mechanics that provides an important nonclassical resource for quantum information and computation. Abramsky and Brandenburger used sheaf theory to give a general treatment of contextuality in quantum theory [New Journal of Physics 13 (2011) 113036]. However, contextual phenomena are found in other fields as well, for example database theory. In this paper, we shall develop this unified view of contextuality. We provide two main contributions: firstly, we expose a remarkable connection between contexuality and logical paradoxes; secondly, we show that an important class of contextuality arguments has a topological origin. More specifically, we show that "AllvsNothing" proofs of contextuality are witnessed by cohomological obstructions. 

10:30  Coffee break (Room H 3005)  
11:00  Sylvain Salvati, Igor Walukiewicz 
A model for behavioural properties of higherorder programs
Show abstract We consider simply typed lambdacalculus with fixpoints as a noninterpreted functional programming language: the result of the execution of a program is its normal form that can be seen as a potentially infinite tree of calls to builtin operations. Properties of such trees are properties of executions of programs and monadic secondorder logic (MSOL) is well suited to express them. For a given MSOL property we show how to construct a finitary model recognizing it. In other words, the value of a lambdaterm in the model determines if the tree that is the result of the execution of the term satisfies the property. The finiteness of the construction has as consequences many known results about the verification of higherorder programs in this framework. 

11:30  Lorenzo Clemente, Sławomir Lasota 
Reachability analysis of firstorder definable pushdown systems
Show abstract We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are firstorder definable in a fixed countablyinfinite structure. We show that the reachability analysis can be addressed with the wellknown saturation technique for the wide class of oligomorphic structures. Moreover, for the more restrictive homogeneous structures, we are able to give concrete complexity upper bounds. We show ample applicability of our technique by presenting several concrete examples of homogeneous structures, subsuming, with optimal complexity, known results from the literature. We show that infinitely many such examples of homogeneous structures can be obtained with the classical wreath product construction. 

12:00  Charles Grellois, PaulAndré Melliès 
Relational Semantics of Linear Logic and Higherorder Model Checking
Show abstract In this article, we develop a new and somewhat unexpected connection between higherorder modelchecking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any higherorder recursion scheme (HORS) comes together with a dual Church encoding of an alternating tree automata (ATA) of the same signature. Moreover, the interaction between the relational interpretations of the HORS and of the ATA identifies the set of accepting states of the tree automaton against the infinite tree generated by the recursion scheme. We show how to extend this result to alternating parity automata (APT) by introducing a parametric version of the exponential modality of linear logic, capturing the formal properties of colors (or priorities) in higherorder modelchecking. We show in particular how to reunderstand in this way the typetheoretic approach to higherorder modelchecking developed by Kobayashi and Ong. We briefly explain in the end of the paper how this analysis driven by linear logic results in a new and purely semantic proof of decidability of the formulas of the monadic secondorder logic for higherorder recursion schemes. 

12:30  Lunch break  
14:00  Juha Kontinen, JulianSteffen Müller, Henning Schnoor, Heribert Vollmer 
A Van Benthem Theorem for Modal Team Semantics
Show abstract The famous van Benthem theorem states that modal logic corresponds exactly to the fragment of firstorder logic that is invariant under bisimulation. In this article we prove an exact analogue of this theorem in the framework of modal dependence logic (MDL) and team semantics. We show that Modal Team Logic (MTL) extending MDL by classical negation captures exactly the FOdefinable bisimulation invariant properties of Kripke structures and teams. We also compare the expressive power of MTL to most of the variants and extensions of MDL recently studied in the area. 

14:30  Katsuhiko Sano, Jonni Virtema 
Axiomatizing Propositional Dependence Logics
Show abstract We give sound and complete Hilbertstyle axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi. 

15:00  Thomas Schwentick, Nils Vortmeier, Thomas Zeume 
Static Analysis for LogicBased Dynamic Programs
Show abstract The goal of dynamic programs as introduced by Patnaik and Immerman (1994) is to maintain the result of a fixed query for an input database which is subject to tuple insertions and deletions. To this end such programs store an auxiliary database whose relations are updated via firstorder formulas upon modifications of the input database. One of those auxiliary relations is supposed to store the answer to the query. Several static analysis problems can be associated to such dynamic programs. Is the answer relation of a given dynamic program always empty? Does a program actually maintain a query? That is, is the answer given of the program the same when an input database was reached by two different modification sequences? Even more, is the content of auxiliary relations independent of the modification sequence that lead to an input database? We study the algorithmic properties of those and similar static analysis problems. Since all these problems can easily be seen to be undecidable for full firstorder programs, we examine the exact borderline for decidability for restricted programs. Our focus is on restricting the arity of the input databases as well as the auxiliary databases, and to restrict the use of quantifiers. 

15:30  Coffee break (Room H 3005)  
16:00  James Brotherston, Jules Villard 
SubClassical Boolean Bunched Logics and the Meaning of Par
Show abstract We investigate intermediate logics between the bunched logics Boolean BI and Classical BI, obtained by combining classical propositional logic with various flavours of Hyland and De Paiva's full intuitionistic linear logic. Thus, in addition to the usual multiplicative conjunction (with its adjoint implication and unit), our logics also feature a multiplicative disjunction (with its adjoint coimplication and unit). The multiplicatives behave "subclassically", in that disjunction and conjunction are related by a weak distribution principle, rather than by De Morgan equivalence. We formulate a Kripke semantics, covering all our subclassical bunched logics, in which the multiplicatives are naturally read in terms of resource operations. Our main theoretical result is that validity according to this semantics coincides with provability in a corresponding Hilbertstyle proof system. Our logical investigation sheds considerable new light on how one can understand the multiplicative disjunction, better known as linear logic's "par", in terms of resource operations. In particular, and in contrast to the earlier Classical BI, the models of our logics include the heaplike memory models of separation logic, in which disjunction can be interpreted as a property of intersection operations over heaps. 

16:30  Stefano Berardi 
Classical and Intuitionistic WellFoundness are Equivalent
Show abstract Assume that we may prove in Classical Functional Analysis that a primitive recursive relation $R$ is wellfounded, using the inductive definition of wellfounded. In this paper we prove that such a proof of wellfoundation may be made intuitionistic. We conclude that if we are able to formulate any mathematical problem as the inductive wellfoundation of some primitive recursive relation, then intuitionistic and classical provability coincide, and for such a statement of wellfoundation we may always find an intuitionistic proof if we may find a proof at all. The core of intuitionism are the methods for computing out data with given properties from input data with given properties: these are the results we are looking for when we do constructive mathematics. Proving that a primitive recursive relation R is inductively wellfounded is a more abstract kind of result, but it is crucial as well, because once we proved that R is inductively wellfounded, then we may write programs by induction over R. This is the way inductive relation are currently used in intuitionism and in proof assistants based on intuitionism, like Coq. In the paper we introduce the comprehension axiom for Functional Analysis in the form of introduction and elimination rules for predicates of types Prop, Nat>Prop, ..., in order to use Girard's method of candidates for impredicative arithmetic. 

17:00  Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi 
Functions out of Higher Truncations
Show abstract In homotopy type theory, the truncation operator n (for a number n greater or equal to 1) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into ntypes, which makes it hard to construct functions An > B if B is not an ntype. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)type, then functions An > B correspond exactly to functions A > B that are constant on all (n+1)st loop spaces. We give one "elementary" proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct "setbased" representations of 1types, as long as they have "braided" loop spaces. The main result with one of its proofs and the application have been formalised in Agda. 

17:30  Murdoch Gabbay, Dan Ghica, Daniela Petrisan 
Leaving the Nest: Nominal techniques for variables with interleaving scopes
Show abstract We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. λx.M) is handled by explicit namecreation and namedestruction brackets (e.g. ⟨x M x⟩) which admit interleaving. We define an appropriate notion of alphaequivalence for such a language and study the syntactic structure required for alphaequivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics. 

20:00  Annual Meeting of the EACSL 