Tuesday, 8 September 2015
|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
Contextuality is a key feature of quantum mechanics that provides an important non-classical 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 "All-vs-Nothing" 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 higher-order programs
We consider simply typed lambda-calculus with fixpoints as a non-interpreted 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 built-in operations. Properties of such trees are properties of executions of programs and monadic second-order 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 lambda-term 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 higher-order programs in this framework.
|11:30||Lorenzo Clemente, Sławomir Lasota||
Reachability analysis of first-order definable pushdown systems
We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are first-order definable in a fixed countably-infinite structure. We show that the reachability analysis can be addressed with the well-known 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, Paul-André Melliès||
Relational Semantics of Linear Logic and Higher-order Model Checking
In this article, we develop a new and somewhat unexpected connection between higher-order model-checking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any higher-order 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 higher-order model-checking. We show in particular how to reunderstand in this way the type-theoretic approach to higher-order model-checking 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 second-order logic for higher-order recursion schemes.
|14:00||Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, Heribert Vollmer||
A Van Benthem Theorem for Modal Team Semantics
The famous van Benthem theorem states that modal logic corresponds exactly to the fragment of first-order 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 FO-definable 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
We give sound and complete Hilbert-style 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 Logic-Based Dynamic Programs
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 first-order 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 first-order 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||
Sub-Classical Boolean Bunched Logics and the Meaning of Par
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 co-implication and unit). The multiplicatives behave "sub-classically", 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 sub-classical 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 Hilbert-style 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 heap-like memory models of separation logic, in which disjunction can be interpreted as a property of intersection operations over heaps.
Classical and Intuitionistic Well-Foundness are Equivalent
Assume that we may prove in Classical Functional Analysis that a primitive recursive relation $R$ is well-founded, using the inductive definition of well-founded. In this paper we prove that such a proof of well-foundation may be made intuitionistic. We conclude that if we are able to formulate any mathematical problem as the inductive well-foundation of some primitive recursive relation, then intuitionistic and classical provability coincide, and for such a statement of well-foundation 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 well-founded is a more abstract kind of result, but it is crucial as well, because once we proved that R is inductively well-founded, 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
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 n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. 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 ||A||n -> 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 "set-based" representations of 1-types, 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
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 name-creation and name-destruction brackets (e.g. ⟨x M x⟩) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence 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|