LCC on Saturday, July 10th

09:00‑10:00 Session 1
Location: AT 2.12
09:00 Ugo Dal Lago
Implicit Complexity in a Concurrency Scenario
10:30‑12:30 Session 2
Location: AT 2.12
10:30 Guillaume Bonfante
Course of value in programming languages

This paper follows a line opened by Bonfante at DICE 2010 where he has shown that transformations of languages could be used to compare sets of programs. Let us come back to the key idea. In the field of implicit computational complexity, when characterizing a set of programs, one usually exhibits some remarkable example, showing thus the strength of the theory. However, the argument is usually rather weak since one has to compare programs, not functions. We point out the work of Asperti who considers such complexity cliques, showing their intrinsic undecidability.

To avoid such direct comparison of programs, we propose to compare sets of programs via some device. Let us suppose that under some transformation (of programs), two sets of programs yield different functions, then, the two initial sets of programs cannot be equivalent from an implicit computational complexity point of view. The transformation works as a kind of lens, separating thus indistinguishable programs at the first level.

We prove that course-of-values is such a device, separating cons-free-programs from programs with a multi-set path ordering termination proof admitting a quasi-interpretation. Both characterize PTIME, but, the transformation of the former characterizes PTIME while the transformation of the latter characterizes PSPACE.

11:00 Stephen Cook and Lila Fontes
Formal Theories for Linear Algebra

We introduce two-sorted theories in the style of [Cook/Nguyen] for the complexity classes ParityL and DET, whose complete problems include determinants over GF(2) and Z, respectively. We then describe interpretations of Soltys' linear algebra theory LAP over arbitrary integral domains, into each of our new theories. The result shows equivalences of standard theorems of linear algebra over GF(2) and Z can be proved in the corresponding theory, but leaves open the interesting question of whether the theorems themselves can be proved.

11:30 Marco Gaboardi and Brian Redmond
Towards a Light Logic for PSPACE

In a previous work, the first author, has proposed a type assignment system correct and complete for the PSPACE complexity class. The logical system obtained by forgetting terms in this type system is unsatisfactory. Indeed, boolean constants in this logic are redundant and, moreover, the key additive rule has no direct translation in a sequent calculus. The second author, in developing the functional language Pola, has observed that when the underlying category is distributive the corresponding type system is complete for PSPACE computations. It is natural to investigate whether this distribution law can be incorporated into the light logic setting to achieve a logical system characterizing PSPACE.

12:00 Pierre Boudes, Damiano Mazza and Lorenzo Tortora de Falco
A Categorical Construction for Linear Logic by Levels

Over the last few years, linear logic has developed a significant link with implicit computational complexity, given by its so-called "light" subsystems. The first example are Girard's light and elementary linear logic (ELL); more recently, Baillot and the second author introduced a generalization of ELL, called linear logic by levels. In this work, we address the question of finding a strict denotational semantics of this system; "strict" meaning that it does not give a denotational semantics of full linear logic. We thus propose a categorical construction that, given a model of linear logic having a property we call weak injectivity, yields a strict denotational semantics of linear logic by levels, which furthermore semantically characterizes the system, in the following sense: a linear logic proof is in linear logic by levels iff its denotational interpretation lies in the model given by our construction. Weak injectivity is a rather mild hypothesis: for example, coherence spaces, the relational model, and finiteness spaces all satisfy it.

14:00‑15:00 Session 3
Location: AT 2.12
14:00 Stephen Cook
Bounded Reverse Mathematics
15:30‑17:30 Session 4
Location: AT 2.12
15:30 Albert Atserias
On Spectral Methods as Refutation Heuristic
16:30 Alexander Rabinovich
Temporal logics over linear time domains are in PSPACE

We investigate the complexity of the satisfiability problem of temporal logics with a finite set of modalities definable in the existential fragment of monadic second-order logic. % We show that the problem is in $\pspace$ over the class of all linear orders. The same techniques show that the problem is in $\pspace$ over many interesting classes of linear orders. %

17:00 Jiamou Liu
Recursion-Theoretic Complexity of \omega-Automatic Trees

The work presented in this talk is joint with Dietrich Kuske and Markus Lohrey. We study \omega-automatic trees. These are trees that can be coded by \omega-words in such a way that their domains and edge relations are recognized by B\"uchi automata. Such a tree is injectively \omega-automatic if each node is represented by a unique \omega-word. We present several results on the complexity of deciding the isomorphism problem for (injectively) \omega-automatic trees of finite height: (i) The isomorphism problem for (injectively) \omega-automatic trees of height 1 (resp. 2) is decidable (resp. \Pi^0_1-complete). (ii) The isomorphism for injectively \omega-automatic trees of height 3 is \Pi^1_1-hard (iii) The isomorphism for injectively \omega-automatic trees of finite height does not belong to the analytical hierarchy. (iv) Assuming CH, The isomorphism problem for injectively \omega-automatic trees of finite height is recursively equivalent to the second-order theory of (\N;+,\times).