I describe array separation logic (ASL), a variant of separation logic in which the data structures are either pointers or arrays. This logic can be used, e.g., to give memory safety proofs of imperative array programs. The key to automatically inferring specifications is the so-called "biabduction" problem, given formulas A and B, find formulas X and Y such that A + X |= B + Y (and such that A + X is also satisfiable), where + is the well-known "separating conjunction" of separation logic. We give an NP decision procedure for this problem that produces solutions of reasonable quality, and we also show that the problem of finding a consistent solution is NP-hard. Along the way, we study satisfiability and entailment in our logic, giving decision procedures and complexity bounds for both problems. This is joint work with Nikos Gorogiannis (Middlesex) and Max Kanovich (UCL).

• Event: Kick-off Meeting for Project TICAMORE (2017)

I will focus on several substructural logics, mainly conservative extensions of the Lambek calculus (associative and nonassociative, with and without constants) and point out some basic open problems. Examples: the lower bound of the complexity of the full nonassociative Lambek calculus, the decidability of Pratt's action logic, the decidability of the consequence relation for the nonassociative Lambek calculus with involutive negations, the decidability of the equational theory of lattice-ordered pregroups. I will briefly discuss what is known in these areas.

• Event: Kick-off Meeting for Project TICAMORE (2017)