Marco Gaboardi, Univ. Buffalo, SUNY. Type systems for the relational verification of higher order programs **Abstract: **Relational program verification is a variant of program verification
where one focuses on guaranteeing properties about the executions of
two programs, and as a special case about two executions of a single
program on different inputs. Relational verification becomes
particularly interesting when non-functional aspects of a computation,
like probabilities or resource cost, are considered. Several
approached to relational program verification have been developed,
from relational program logics to relational abstract interpretation.
In this talk, I will introduce two approaches to relational program
verification for higher-order computations based on the use of type
systems. The first approach consists in developing powerful type
system where a rich language of assertions can be used to express
complex relations between two programs. The second approach consists
in developing more restrictive type systems enriched with effects
expressing in a lightweight way relations between different runs of
the same program. I will discuss the pros and cons of these two
approaches on a concrete example: relational cost analysis, which aims
at giving a bound on the difference in cost of running two programs,
and as a special case the difference in cost of two executions of a
single program on different inputs.

Georg Moser, Univ. Innsbruck. Uniform Resource Analysis by Rewriting: Strengths and Weaknesses **Abstract: **In this talk, I'll describe how rewriting techniques can be
successfully employed to built state-of-the-art automated resource
analysis tools which favourably compare to other
approaches. Furthermore I'll sketch the genesis of a uniform framework
for resource analysis, emphasising success stories, without hiding
intricate weaknesses. The talk ends with the discussion of open
problems.

Alexandra Silva, UCL. Brzozowski Goes Concurrent — A Kleene Theorem for Pomset Languages **Abstract: **Concurrent Kleene Algebra (CKA) is a mathematical formalism to study
programs that exhibit concurrent behaviour. As with previous
extensions of Kleene Algebra, characterizing the free model is crucial
in order to develop the foundations of the theory and potential
applications. For CKA, this has been an open question for a few years
and this talk will overview why the problem is so difficult. We will
then pave the way towards a solution, by presenting a new automaton
model and a Kleene-like theorem for CKA. More precisely, we connect a
relaxed version of CKA to series-parallel pomset languages, which are
a natural candidate for the free model. There are two substantial
differences with previous work: from expressions to automata, we use
Brzozowski derivatives, which enable a direct construction of the
automaton; from automata to expressions, we provide a syntactic
characterization of the automata that denote valid CKA behaviours. We
also survey how the present work can be used to to extend the network
specification language NetKAT with primitives for concurrency so as to
model and reason about concurrency within networks. This is joint work
with Tobias Kappe, Paul Brunet, Bas Luttik, and Fabio Zanasi.

Christine Tasson, Univ. Paris Diderot. Quantitative semantics for probabilistic programming **Abstract: **Probabilistic programming has many applications in statistics,
physics,... so that all programming languages have been equipped with
probabilistic library. However, there is a need in developing
semantical tools in order to formalize higher order and recursive
probabilistic languages. Indeed, it is well known that categories of
measurable spaces are not Cartesian closed. We have been studying
quantitative semantics of probabilistic spaces to fill this gap. A
first step has been to focus on probabilistic programming languages
with discrete types such as integers and booleans. In this setting,
probabilistic programs can be seen as linear combinations of
deterministic programs. Probabilistic Coherent Spaces constitute a
Cartesian closed category that is fully abstract with respect to
probabilistic Call-By-Push-Value. Moreover, this toy language is
endowed with a memorization operator that allow to encode most
discrete probabilistic programs. The second step is to move on
probabilistic programming with continuous types representing for
instance reals endowed with Lebesgue measurable sets. We introduce the
category of cones and stable functions which is Cartesian closed. The
trick is to enlarge the category of measurable spaces to gain
closeness and to embrace measurable spaces. Besides, the category of
cones is a sound and adequate model of a higher order and recursive
probabilistic language in which most classical distributions and
probabilistic tools can be encoded. This is joint work with Thomas
Ehrhard and Michele Pagani.