---------------------------------------------------------------------- INVITED TALK Computation by Interaction for Structuring Low-Level Languages Ulrich Schoepp (LMU Munich) A successful approach in the semantics of programming languages is to model programs by interaction dialogues. While dialogues are most often considered as abstract mathematical objects, it has also been argued that they are useful for actual computation. Dialogues have been found useful especially for resource bounded computation, e.g. in Ghica's recent approach to hardware synthesis, or in joint work with Dal Lago on programming with sublinear space. In this talk I will consider computation by interaction as an approach to organising and structuring low-level languages. The starting point is a simple way of constructing a basic interactive computation model from a low-level language by means of the Int-construction. Even for weak languages, the thus constructed model has interesting structure. It supports higher order functions and control effects, but also allows for fine-grained control of space usage. The model construction is not only related to game semantics, but it also turns out to be closely related to well-known methods of compiling with continuations and defunctionalization. This motivates further investigations, such as into how to account for low-level languages with computational effects. ----------------------------------------------------------------------

Algorithmic Games for Full Ground References Nikos Tzevelekos (Queen Mary, University of London) and Andrzej Murawski (University of Leicester) We present a full classification of decidable and undecidable cases for contextual equivalence in a finitary ML-like language equipped with full ground storage (both integers and reference names can be stored). The simplest undecidable type is unit -> unit -> unit. At the technical level, our results marry game semantics with automata-theoretic techniques developed to handle infinite alphabets. On the automata-theoretic front, we show decidability of the emptiness problem for register pushdown automata extended with fresh-symbol generation. ----------------------------------------------------------------------

Kripke Logical Relations for Region Polymorphism Jacob Thamsborg (ITU Copenhagen), Lars Birkedal (ITU Copenhagen), Guilhem Jaber (Ecole des Mines de Nantes) and Filip Sieczkowski (ITU Copenhagen) In this talk, we will define logical relations for an effect type system with region polymorphism. To do so, we will introduce a restricted version of polymorphism, so that a good notion of equivalence of programs can be defined. ----------------------------------------------------------------------

Extending Nakano-style Type Systems and Logics Tadeusz Litak (University of Leicester) Nakano's 2000 LiCS and 2001 TACS papers alerted the typing community to the use of Loeb-style modalities a) for ensuring productivity of guarded (co-)recursion, b) in the (meta-)theory of logical step-indexed relations and c) reactive programming. Much subsequent research has been done since in the area; it is enough to mention Appel et al. (POPL'07), Birkedal et al. (LiCS'11, POPL'11, FiCS'10), Krishnaswami&Benton (LiCS'11, ICFP'11), Krishnaswami et al. (POPL'12), Benton and Tabareau (TLDI'09) or Jaber et al. (LiCS'12). The success story of these modalities ultimately relies on the fact that in the presence of the Loeb axiom, the addition of an explicit fixed point-operator does not increase the expressive power of the modal fragment - assuming that all occurrences of the bound variable are guarded by the modal operator. Each such formula has an explicitly computable fixed point in the purely modal fragment. Furthermore, this fixed point is unique (up to logical equivalence). This has been proved in the 1970's (!) by Sambin and, independently, by de Jongh. This three-decade gap suggests that research in modal logic may still have more to offer the typing community. In this talk (a work in progress), I am going to describe two ways in which Nakano-style use of modalities can be improved: 1) Some stronger variants of Nakano's typing systems (he proposed more than one) implicitly assume logical principles which are completely independent from the Loeb axiom, in particular a kind of "Cantor-Bendixson axiom" (CB for short). This principle also happens to hold in the internal language of the topos of trees of Birkedal et al---probably the most successful model of guarded recursion so far. The computational meaning of CB is not related not so much to guarded recursion, but - as it turns out - to *guarded continuations/control operators*. 2) In the recent decade, the modal logic community extended the results of Sambin and de Jongh to fixed-point calculi over the Loeb logic where the requirement that all occurrences of the bound variable is guarded by modalities is significantly relaxed. As proved by Visser and Van Benthem, *over the classical logic* Sambin-de Jongh theorem can be extended to formulas where every non-guarded occurrence of variable is positive. The only caveat is that fixed points obtained this way are not necessarily unique. The full generality of the Visser-Van Benthem result requires some essentially classical principles. But, as it turns out, it is possible to prove a constructive counterpart of it. The constructive variant is based on a new class of "locally inflationary" formulas, strictly extending both guarded and *strictly positive* ones. As it turns out, locally inflationary formulas work more naturally with greatest rather than smallest fixed points. ----------------------------------------------------------------------

INVITED TALK Reasoning Formally About Weak Memory from Testing Jade Alglave (University of Oxford) We present a class of relaxed memory models, defined in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and the visibility of inter- and intra-processor communications through memory (e.g. store atomicity relaxation). We prove results on the required behaviour and placement of memory fences to restore a given model (such as Sequential Consistency) from a weaker one. Based on this class of models we develop a tool, diy, that systematically and automatically generates and runs litmus tests to determine properties of processor implementations. We detail the results of our experiments on Power and the model we base on them. This work identified a rare implementation error in Power 5 memory barriers (for which IBM is providing a workaround); our results also suggest that Power 6 and 7 do not suffer from this problem. This is joint work with Luc Maranget, Susmit Sarkar and Peter Sewell ----------------------------------------------------------------------

Using Coq to Generate and Reason About x86 Systems Code Nick Benton (Microsoft Research), Andrew Kennedy (Microsoft Research) and Jonas Jensen (ITU Copenhagen) The talk describes some in-progress work on modelling, generating and reasoning about x86 code within the Coq proof assistant. This work is part of a larger project on compositional verification of high-level behavioural properties of low-level systems code, such as schedulers, memory managers, loaders and verifiers. ----------------------------------------------------------------------

Subjective Concurrent Separation Logic Ruy Ley-Wild (IMDEA Software) and Aleksandar Nanevski (IMDEA Software) From Owicki-Gries' resource invariants and Jones' rely/guarantee to modern variants based on separation logic, axiomatic program logics for concurrency have a limited form of compositionality. Proving non-trivial properties usually requires the use of auxiliary state, which is ``objective'' in the sense that each thread's auxiliary state is given a globally-unique name. Since auxiliary state exposes the program's global structure to each local thread, axiomatic approaches fail to be compositional in the presence of auxiliary state. We propose ``subjective'' auxiliary state as a solution to this historical limitation of axiomatic program logics. Each thread can be verified with a subjective view on auxiliary state: auxiliary state can be partitioned to either belong to the \emph{self} (\ie, the thread itself) or to the \emph{other} (\ie, its environment). We formulate Subjective Concurrent Separation Logic as a combination of the resource invariant method, separation logic, and subjective auxiliary state for a first-order, stateful, concurrent language. The logic provides compositional verification even when auxiliary state is needed. We give an operational proof of soundness. ----------------------------------------------------------------------

Strong Monads and Enriched Adjunctions Paul-Andre Mellies (CNRS and University Paris Diderot) Starting from the particular case of the double negation monad in dialogue categories, we investigate what additional structure is required of an adjunction in order to give rise to a strong monad. The analysis leads to a purely combinatorial reformulation of enriched functors, enriched natural transformations and enriched adjunctions between categories equipped with a monoidal action. ----------------------------------------------------------------------