|
Thursday, 9 February
|
|
9:15 - 9:30
|
Welcome
|
|
9:30 - 10:30
|
Mikołaj Bojańczyk Automata with data values and nominal sets
|
|
|
This talk claims that nominal sets are a unified framework that
describes various kinds of automata over data words. Nominal sets are
a different kind of set theory, originating in the work of Mostowski
and Fraenkel, and appearing in computer science thanks to Gabbay and
Pitts. The definition of a set is different, and crucially, the
definition of a finite set is different. In the world of nominal sets,
for instance, the alphabet used in data words is a finite alphabet. I
will show that in nominal sets, the standard definitions of automata
yield various kinds of automata for data words, mainly variants of
Kaminski and Francez automata.
|
|
10:30 - 11:00
|
Coffee break
|
|
11:00 - 11:40
|
Nikos Tzevelekos Games with names
|
|
|
This talk is about formal reasoning techniques for programming languages with names which have emerged in the last years. We will focus on game semantics, and in particular nominal game semantics. The latter constitutes a fresh strand of the theory, founded on nominal sets of Gabbay and Pitts, which provides models for programming languages with new resources such as fragments of ML. Moreover, nominal game models can be given algorithmic representations by means of newly introduced abstract machines, called Fresh-Register Automata, which operate on infinite alphabets of names and extend ordinary Register Automata.
|
|
11:40 - 12:20
|
Andrzej Murawski Algorithmic games for ground storage
|
|
|
We investigate a finitary ML-like language equipped with primitives for storing
reference names. Using game semantics and automata-theoretic techniques
we provide a complete characterization of cases in which contextual equivalence
is decidable.
|
|
12:20 - 13:00
|
Ugo Montanari A network-conscious extension of pi-calculus
|
|
|
Traditional process calculi usually abstract away from network details, modelling only communication over shared channels. They, however, seem inadequate to describe new network architectures, such as Software Defined Networks, where programs are allowed to manipulate the infrastructure. In this talk we present a network conscious, proper extension of the pi-calculus: we add connector names and primitives to handle them. We also hint to a coalgebraic semantics in the style of Fiore, Turi and Staton, where a saturated semantics is derived categorically. (Joint work with Matteo Sammartino) |
|
13:00 - 14:30
|
Lunch
|
|
14:30 - 15:10
|
Sławomir Lasota Nominal computation
|
|
|
This talk is an attempt at defining computation in nominal sets. I present a rudimentary programming language called Nlambda. The key idea is that it includes a native type for finite sets in the nominal sense. To illustrate the power of this language, I write short programs that process automata on data words.
|
|
15:10 - 15:50
|
Ranko Lazic On Petri nets with a stack
|
|
|
These systems can be seen as models of programs with unbounded integers and recursion, and are also closely related to a first-order logic with two variables on data trees. Atig and Ganty have recently shown that
the notion of index of a context-free language can be used to restrict
the systems so that they become equivalent to Reinhardt's Petri nets with weak inhibitor arcs, and therefore have decidable reachability.
We provide a lower bound for reachability for the unrestricted Petri nets with a stack, whose decidability remains an open problem.
|
|
15:50 - 16:30
|
Coffee break
|
|
16:30 - 17:10
|
Christian Urban Nominal techniques in Isabelle
|
|
17:10 - 18:00
|
Discussion
|
|
Friday, 10 February
|
|
9:00 - 9:40
|
Bartek Klin Nominal sets on structured data
|
|
|
I describe a generalization of nominal sets to a situation where atoms (or data values) come equipped with a first-order relational structure that can be checked upon. Mathematically, this amounts to considering subgroups of data bijections. Some parts of Gabbay-Pitts' theory of nominal sets work without change in this nominal setting. Other parts, such as the existence of least supports, depend on further assumptions on the relational structure in question.
|
|
9:40 - 10:20
|
Szymon Toruńczyk Automata over non-homogeneous structures
|
|
|
We describe a rudimentary framework for dealing with automata which work over structures which are non-homogeneous, such as (Z,<). The approach is to consider actions of inverse semigroups.
|
|
10:20 - 10:50
|
Coffee break
|
|
10:50 - 11:30
|
Alexander Kurz/Emilio Tuosto On nominal regular languages with binders
|
|
|
We investigate regular languages on infinite alphabets where words
may contain binders on names. To this end, classical regular expressions and
automata are extended with binders. We prove the equivalence between finite
automata on binders and regular expressions with binders and investigate
closure
properties and complementation of regular languages with binders.
|
|
11:30 - 12:10
|
Vincenzo Ciancia Stream automata are coalgebras
|
|
|
Stream automata (also called omega-automata), and omega-regular
languages, are of paramount importance in
Computer Science and Logic. A coalgebraic treatment of these structures has not
been given yet.
We study a simple two-sorted setting where deterministic Muller
automata can be cast
as coalgebras, so that coalgebraic bisimilarity coincides with
language equivalence.
From this characterisation, we derive concise and natural decision
procedures for
complementation, union, intersection, and equivalence check.
Once a coalgebraic formulation has been established, one may seek for
generalisations e.g. by extending the base category. Stream automata
over nominal sets would be a direct application of the developed
framework.
|
|
12:10 - 12:30
|
Closing remarks
|
|
12:30 - 14:00
|
Lunch
|
