----------------------------------------------------------------------
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.
----------------------------------------------------------------------