-
Building on previous results concerning the functorial
semantics of partial and multi-algebras, the talk discusses
the category of free semi-modules over a semiring (considered
as the Kleisli category of the semiring monad). At first, it
is proved that such Kleisli category is gs-monoidal (i.e., it
is symmetric monoidal and each object has a comonoid
structure), whenever the underlying category is cartesian:
hence, it represents a suitable semantical domain for
multi-algebras. Furthermore, and more important, two arrows
of the freely generated gs-monoidal category are shown to be
isomorphic iff they are identified by every possible
intepretation in the category of free semi-modules for the
semiring of natural numbers.
-
11: break
-
Symmetric monoidal categories provide a foundational formalism
for a variety of important domains, including quantum
computation. These categories have a natural visualisation as a
form of graphs. I will present a formalism for equational
reasoning about such graphs and develop this into a generic
proof system with a fixed logical kernel. A salient feature of
our system is that it provides a formal and declarative account
of derived results that can include 'ellipses'-style
notation. I will illustrate the framework by describing the
graphical language applied to quantum computation and boolean
circuits, and show how this can be used to perform computations
symbolically.
-
13: lunch
-
14 (G4): Reiko Heckel - The Trouble with Names in Graph
Transformation
In the standard categorical approach to graph
transformation, the result of a rule application is only defied
up to isomorphism. Rightly or wrongly, this leads to the
perception that graphs should be considered up to isomorphism,
ignoring the concrete names of their nodes and edges. We
discuss some of the problems arising from this interpretation,
touching on concurrent semantics, stochastic model checking and
hint on the (sometimes ad-hoc) solutions.
-
15 (G4): Tomoyuki Suzuki - Nominal Kleene Algebra
(joint work with Alexander Kurz and Emilio Tuosto)
It is well known that Kleene algebras, finite automata and
regular languages are considered as fundamental tools to
describe machines and to analyse computation in Computer
science. Nowadays, however, the meaning of machines or
computations starts to contain "communications", "security" or
"resources". In other words, computer is not only a stand alone
machine but also a dynamic system which is sensitive to its own
environment. Through this research, we try to capture the
relatively new notion of machines with Nominal algebras, which
allow us to clarify local and global information for each
computer. In this talk, I will present our nominal languages,
automata with names and Nominal Kleene algebras.
-
16 (G4): Alexander Kurz - Universal Algebra over Nominal Sets
-
-
11 (G4): Paolo Torrini - Linear Logic for Graph
Transformation
We are looking into a way to represent name restriction as
resource-bound quantification and DPO graph transformation as
linear consequence relation, relying on a first-order variant of
intuitionistic linear logic with proof terms.
Organisers: Reiko Heckel, Alexander Kurz, Paolo Torrini, Emilio
Tuosto