BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Google Inc//Google Calendar 70.9054//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
DESCRIPTION:Graph Transformation Theory and Applications seminar of IRIF
NAME:Graph Transformation Theory and Applications
REFRESH-INTERVAL:PT4H
TIMEZONE-ID:Europe/Paris
X-WR-CALDESC:Graph Transformation Theory and Applications seminar of IRIF
X-WR-CALNAME:Graph Transformation Theory and Applications
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:Graph Transformation Meets Logic - Barbara König\, Fakultät für
Ingenieurwissenschaften\, Universität Duisburg-Essen\, Germany
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201120T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201120T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1236
DESCRIPTION:We review the integration of (first-order) logic respectively
nested conditions into graph transformation. Conditions can serve various
purposes: they can constrain graph rewriting\, symbolically specify sets o
f graphs\, be used in query languages and in verification (for instance in
Hoare logic and for behavioural equivalence checking). \n\nIn the graph t
ransformation community the formalism of nested graph conditions has emerg
ed\, that is\, conditions which are equivalent to first-order logic\, but
directly integrate graphs and graph morphisms\, in order to express constr
aints more succinctly. \n\nIn this talk we also explain how the notion of
nested conditions can be lifted from graph transformation systems to the s
etting of reactive systems as defined by Leifer and Milner. It turns out t
hat some constructions for graph transformation systems (such as computing
weakest preconditions and strongest postconditions and showing local conf
luence by means of critical pair analysis) can be done quite elegantly in
the more general setting.\n\n[[https://www.youtube.com/watch?v=8gGWdbRt4U8
|video recording of the seminar on YouTube]]
LOCATION:(online)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chemical Graph Transformation and Applications - Daniel Merkle & J
akob Lykke Andersen\, Department of Mathematics and Computer Science\, Uni
versity of Southern Denmark\, Odense\, Denmark
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201204T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201204T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1237
DESCRIPTION:Any computational method in chemistry must choose some level o
f precision in the modeling. One choice is made in the methods of quantum
chemistry based on quantum field theory. While highly accurate\, the metho
ds are computationally very demanding\, which restricts their practical us
e to single reactions of molecules of moderate size even when run on super
computers. At the same time\, most existing computational methods for syst
ems chemistry and biology are formulated at the other abstraction extreme\
, in which the structure of molecules is represented either not at all or
in a very rudimentary fashion that does not permit the tracking of individ
ual atoms across a series of reactions.\n\nIn this talk\, we present our o
n-going work on creating a practical modelling framework for chemistry bas
ed on Double Pushout graph transformation\, and how it can be applied to a
nalyse chemical systems. We will address important technical design decisi
ons as well as the importance of methods inspired from Algorithm Engineeri
ng in order to reach the required efficiency of our implementation. We wil
l present chemically relevant features that our framework provides (e.g. a
utomatic atom tracing) as well as a set of chemical systems we investigate
d are currently investigating. If time allows we will discuss variations o
f graph transformation rule compositions and their chemical validity.\n\n\
n[[https://www.youtube.com/watch?v=mzIXfsp-eJE&t=337s|video recording of t
he seminar on YouTube]]
LOCATION:(online)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hierarchical port graphs & PORGY - port graph rewriting as a model
ling tool - Maribel Fernandez & Bruno Pinaud\, King's College London\, UK
& Université de Bordeaux\, France
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201218T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201218T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1238
DESCRIPTION:Graph rewriting systems are natural verification and validatio
n tools: they provide visual\, intuitive representations of complex system
s while specifying the dynamic behaviour of the system in a formal way. In
this talk we will describe the use of strategic port graph rewriting as a
basis for the implementation of a visual modelling tool: PORGY. We will p
resent attributed hierarchical port graphs (AHP) and a notion of strategic
AHP-rewriting as a mechanism to model the behaviour of dynamic systems. T
he system modelled is represented by an initial graph and a collection of
graph rewrite rules\, together with a user-defined strategy to control the
application of rules. The traditional operators found in strategy languag
es for term rewriting have been adapted to deal with the more general sett
ing of graph rewriting\, and some new constructs have been included in the
strategy language to deal with graph traversal and management of rewritin
g positions in the graph. In the second part of the talk\, we describe POR
GY and give examples of application in the areas of biochemistry\, social
networks and finance.\n\nThis is joint work with members of the PORGY team
at Bordeaux and King’s College London.\n\n\n[[https://youtu.be/D_YHlXaw
g9o|YouTube live recording of the seminar]]
LOCATION:(online)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Java Bytecode Verification and Manipulation based on Model Driven
Engineering - Christoph Bockisch & Gabriele Taentzer\, Fachbereich Mathema
tik und Informatik\, Philipps-Universität Marburg\, Germany
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210115T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210115T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1239
DESCRIPTION:Program transformations are frequently developed\, e.g.\, to r
ealize programming language extensions or dynamic program analyses such as
profiling. They are typically implemented by manipulating bytecode as the
availability of source code is not guaranteed. There are standard librari
es such as ASM that are typically used for implementing Java bytecode mani
pulations. To check their correctness\, they are usually tested by applyin
g them to different programs\, running the manipulated programs and observ
ing their behaviors. As part of the second step\, the Java virtual machine
verifies the bytecode\, which can uncover errors in the bytecode introduc
ed by the manipulation. That approach uses different technologies that are
not well linked making the process of developing and testing bytecode man
ipulations difficult. In this talk\, we intend to perform bytecode manipul
ation by using concepts and techniques of model-driven engineering. We are
convinced that the declarative nature of model transformation rules allow
s the debugging and analyzing of bytecode manipulations in more details th
an classically done. Following this path\, a meta-model for bytecode is ne
eded including OCL constraints for bytecode verification. We show that bas
ing bytecode manipulation on model transformation can provide more immedia
te guidance and feedback to the developer\, especially when model transfor
mation is formally based on graph transformation. Bytecode verification ca
n take place directly in the manipulated model with the help of OCL checki
ng\, eliminating the need to use multiple technologies. In some cases\, it
is even possible to automatically determine application conditions under
which bytecode manipulations are correct by construction\; then bytecode v
erification after a bytecode manipulation can be avoided altogether.\n\n\n
[[https://youtu.be/glboPhoWFXw|YouTube live recording of the seminar]]
LOCATION:(online)
END:VEVENT
BEGIN:VEVENT
SUMMARY:MDEOptimiser: Searching for optimal models with EMF and Henshin -
Alexandru Burdusel & Steffen Zschaler\, Department of Informatics\, King's
College London\, UK
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210212T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210212T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1240
DESCRIPTION:An overview presentation of the work we have been doing over t
he past years on MDEOptimiser\, a tool that uses evolutionary search over
EMF models to solve multi-objective optimisation problems. Graph transform
ations are used to encode mutation operators\, opening interesting opportu
nities for automatically generating domain-specific mutation operators.\n\
n[[https://youtu.be/vJIx15j4c0g|YouTube live recording]]
LOCATION:(online)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fast Graph Programs - Detlef Plump & Graham Campbell\, University
of York\, UK & Newcastle University\, UK
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210226T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210226T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1241
DESCRIPTION:This will be an overview of our ongoing work on fast graph pro
grams in the language GP 2. We will present programs which in some cases m
atch the time complexity of graph algorithms in imperative languages. In o
ther cases we need to assume that input graphs have a bounded degree\, to
reach the speed of conventional algorithms.\n\n[[https://youtu.be/mYI3Gwji
UW0|YouTube live stream recording]]
LOCATION:(online)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Confluence of Graph Transformation - Leen Lambers & Fernando Oreja
s\, Hasso-Plattner-Institut Potsdam\, Germany & Technical University of Ca
talonia (UPC)\, Spain
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210129T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210129T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1251
DESCRIPTION:Confluence has been studied for graph transformation since sev
eral decades now. Confluence analysis has been applied\, for example\, to
determining uniqueness of model transformation results in model-driven en
gineering. It is strongly related to conflict analysis for graph transfor
mation\, i.e. detecting and inspecting all possible conflicts that may occ
ur for a given set of graph transformation rules. The latter finds applica
tions\, for example\, in software analysis and design. Both conflict and
confluence analysis rely on the existence and further analysis of a finite
and representative set of conflicts for a given set of graph transformati
on rules.\n\nTraditionally\, the set of critical pairs has been shown to c
onstitute such a set. It is representative in the sense that for each conf
lict a critical pair exists\, representing the conflict in a minimal conte
xt\, such that it can be extended injectively to this conflict (M-complete
ness). Recently\, it has been shown that initial conflicts constitute a co
nsiderably reduced subset of critical pairs\, being still representative i
n a slightly different way. In particular\, for each conflict there exist
s a unique initial conflict that can be extended (possibly non-injectively
) to the given conflict (completeness). Compared to the set of critical p
airs\, the smaller set of initial conflicts allows for more efficient conf
lict as well as confluence analysis.\n\nWe continue by demonstrating that
initial conflicts (critical pairs) are minimally complete (resp. minimally
M-complete)\, and thus are both optimally reduced w.r.t. representing con
flicts in a minimal context via general (resp. injective) extension morphi
sms. We proceed with showing that it is impossible to generalize this resu
lt to the case of rules with application conditions (equivalent to FOL on
graphs). We therefore revert to a symbolic setting\, where finiteness and
minimal (M-)completeness can again be guaranteed. Finally\, we describe
important special cases (e.g. rules with negative application conditions)\
, where we are able to obtain minimally complete (resp. M-complete) sets o
f conflicts in the concrete setting again.\n\n\n[[https://youtu.be/Um90A_l
k4ik|YouTube live recording of the seminar]]
LOCATION:(online)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Composition-based Graph Rewriting - Jean-Pierre Jouannaud\, Labora
toire d'Informatique (LIX)\, École Polytechnique
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210312T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210312T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1252
DESCRIPTION:Double Pushout (DPO) rewriting\, the dominant model for graph
rewriting\, emerged in the early 70’s\, strongly influenced at that time
by graph grammars. Developed by Hartmut Ehrig and his many collaborators\
, graph rewriting was from the beginning based on category theory\, with t
he major insight that the two basic rewriting constructions\, namely match
ing and replacement\, were intimately related to graph morphisms and their
pushouts. A new model has emerged recently\, so-called Composition based
rewriting (Core)\, in which rewriting is based on a composition operator o
ver directed rooted labelled graphs (drags)\, so that matching a drag G ag
ainst a drag L amounts to compose L with some context drag C\, and rewriti
ng G with L -> R to compose R with C. We will describe Core for drags befo
re to relate it precisely to DPO and extend it to adhesive categories of g
raphs and beyond. We will also show how to define composition abstractly i
n any category of graphs satisfying appropriate properties among which adh
esivity (wrt monomorphisms). Major differences between DPO and Core will b
e discussed. \n\n\n\n[[https://youtu.be/7Shd5RIcGd8|YouTube live stream re
cording]]
LOCATION:(online)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Formal Graph Language Theory & Fusion Grammars - Hans-Jörg Kreows
ki & Aaron Frederick Lye\, University of Bremen\, Germany
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210326T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210326T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1304
DESCRIPTION:In the first part of the presentation\, some aspects of formal
graph language theory are discussed. A few variants of graph grammars wer
e introduced in the early 1970s as generalizations of Chomsky grammars. Th
is first step into a formal graph language theory was further developed by
the investigation of edge and hyperedge replacement on one hand and on so
me variants of node replacement on the other hand starting in the late 197
0s. Since then\, a good number of structural and decidability properties w
ere proved. In particular\, it turned out that hyperedge replacement gramm
ars behave to a large degree in a context-free manner. In the second part
of the presentation\, the novel approach of fusion grammars is surveyed.\n
\nA fusion grammar is a hypergraph grammar which provides a start hypergra
ph of small connected components. To derive hypergraphs\, connected compon
ents can be copied multiple times and can be fused by the application of f
usion rules (where such an application removes two complementary hyperedge
s and merges their attachment vertices). The generated hypergraph language
contains all terminal connected components of derived hypergraphs. The ma
in results for various kinds of fusion grammars concern their generative p
ower.\n\n\n\n[[https://youtu.be/142aNpKPv04|YouTube live stream recording]
]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hypergraph Rewriting and the Wolfram Model - Jonathan Gorard\, Uni
versity of Cambridge and Wolfram Research\, UK
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210409T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210409T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1333
DESCRIPTION:This talk will summarize some recent results obtained in conne
ction with the Wolfram Physics Project: a systematic attempt to reduce fun
damental physics to the problem of hypergraph rewriting. Specifically\, we
will discuss the construction of an efficient hypergraph rewriting scheme
using the formalism of Wolfram model multiway systems\, with a categorica
l semantics defined via double-pushout rewrites over selective adhesive ca
tegories\, and equipped with a dagger-symmetric monoidal structure that ex
hibits surprising formal connections to categorical quantum mechanics. We
will also demonstrate that\, by equipping such a multiway system with an a
dditional notion of causal structure (defined via the semantics of precaus
al categories)\, we are able to introduce new inference rules of selective
resolution\, paramodulation and factoring that generalize the standard Kn
uth-Bendix completion rules for term rewriting systems\, and significantly
improve the efficiency of automated diagrammatic reasoning algorithms ove
r hypergraphs. Time permitting\, we will discuss some near-term practical
applications of these methods for quantum information theory (allowing for
more efficient diagrammatic simplification of quantum circuits)\, as well
as numerical general relativity (allowing for more explicit numerical sim
ulation of graph-theoretic models of space and time).\n\n\n\n[[https://you
tu.be/TJ5RkdGObGE|YouTube recording]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rewriting Modulo Symmetric Monoidal Structure - Paweł Sobociński
\, Department of Computer Science\, Tallinn University of Technology\, Est
onia
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210423T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210423T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1334
DESCRIPTION:String diagrams are an elegant\, convenient and powerful synta
x for arrows of symmetric monoidal categories. In recent years\, they have
been used as compositional descriptions of computational systems from var
ious fields\, including quantum foundations\, linear algebra\, control the
ory\, automata theory\, concurrency theory\, and even linguistics. All of
these applications rely on diagrammatic reasoning\, which is to string dia
grams as equational reasoning is to ordinary terms. \n\nIf we are to take
string diagrams out of research papers and into practical applications\, w
e need understand how to implement diagrammatic reasoning. This is the foc
us of my talk. \n\nThere is a tight correspondence between symmetric monoi
dal categories where every object has a coherent special Frobenius algebra
structure and categories of cospans of hypergraphs. This correspondence\,
therefore\, takes us from a topological understanding of string diagrams
to a combinatorial data-structure-like description. Moreover\, diagrammati
c reasoning translates via this correspondence exactly to DPO rewriting wi
th interfaces. \n\nThe obvious follow-up question is: how much of this cor
respondence survives if we drop the assumption about Frobenius structure?
Can we use this correspondence to implement diagrammatic reasoning on vani
lla symmetric monoidal categories? The answer is yes\, but we need to rest
rict the kinds of cospans we consider: the underlying hypergraph has to be
acyclic and satisfy an additional condition called monogamy. Moreover\, w
e must restrict the DPO rewriting mechanism to a variant that we call conv
ex DPO rewriting. The good news is that none of these modifications come w
ith a significant algorithmic cost. \n\nThe material in this talk is joint
work with Filippo Bonchi\, Fabio Gadducci\, Aleks Kissinger and Fabio Zan
asi\, and has been published in a series of papers:\n\n- "Rewriting modulo
symmetric monoidal structure"\, Proceedings of LiCS 2016\n\n- "Confluence
of Graph Rewriting with Interfaces"\, Proceedings of ESOP 2017\n\n- "Rewr
iting with Frobenius"\, Proceedings of LiCS 2018\n\n\n\n[[https://youtu.be
/nTWdbm19CFM|YouTube recording]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:GReTA Special Event: Graph Rewriting as a Foundation for Science a
nd Technology (and the Universe) - Stephen Wolfram\, Wolfram Research\, Ch
ampaign\, USA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210428T180000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210428T190000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1361
DESCRIPTION:About the speaker:\n\nStephen Wolfram is the creator of Mathem
atica\, Wolfram|Alpha and the Wolfram Language\; the author of "A New Kind
of Science"\; the originator of the Wolfram Physics Project\; and the fou
nder and CEO of Wolfram Research. Over the course of more than four decade
s\, he has been a pioneer in the development and application of computatio
nal thinking—and has been responsible for many discoveries\, inventions
and innovations in science\, technology and business.\n\n[[https://zoom.us
/meeting/register/tJcrcuipqjoqEtVlOUZXdaCvjXaXWJfVtQpg|Zoom registration]]
\n\n[[https://youtu.be/CLXyDCISsUY|YouTube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Computational Categorical Algebra with Catlab - James Fairbanks\,
Department of Computer & Information Science & Engineering\, University of
Florida\, USA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210507T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210507T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1380
DESCRIPTION:A vast swath of computation and computer science theory takes
place on combinatorial data structures\, which are often presented as vari
ations on the theme of graphs. Catlab.jl is a Julia package for computatio
nal category theory\, which includes an implementation of C-Sets\, also kn
own as copresheafs or category actions. C-Sets always form an adhesive cat
egory and can be used for general rewriting systems. This talk will presen
t the theory and implementation of C-Sets along with some examples. In par
ticular\, Colored Graphs and String Diagrams (syntax for symmetric monoida
l categories) will be shown.\n\n\n[[https://zoom.us/meeting/register/tJcpc
e2prj0oHNJebgHQycRbgG-37P-MD4Ay|Zoom registration]]\n\n[[https://youtu.be/
JSJ-DD_dcjk|YouTube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:From Petri Nets to Graph Rewriting Systems: aspects of truly concu
rrent semantics - Andrea Corradini\, Computer Science Department\, Univers
ity of Pisa\, Italy
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210521T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210521T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1385
DESCRIPTION:Graph rewriting systems are naturally endowed with a notion of
parallelism due to the locality of the effect of rules. These aspects hav
e been studied in the classical theory from an interleaving perspective\,
based on sequential independence\, shift equivalence and related notions.
In the last three decades the theory has been enriched with notions\, cons
tructions and results which provide a direct account of causality and non-
determinism in graph derivations\, borrowed from (and extending) the theor
y of Petri Nets. In the talk I will present a personal overview of the dev
elopment of this theory starting from the basic structural relation betwee
n nets and graph rewriting systems\, and I will survey some more recent de
velopments.\n\n\n[[https://zoom.us/meeting/register/tJAudemsqTIjG9bAbHjVGy
XbvOkDOrNLYTVC|Zoom registration]]\n\n[[https://youtu.be/dgALP6quK1o|YouTu
be live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Global Order Routing on Exchange Networks - Vincent Danos\, CNRS &
Ecole Normale Supérieure\, Paris\, France
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210604T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210604T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1394
DESCRIPTION:We propose an abstract notion of networks of exchanges modelli
ng the global money market of decentralised finance. We formalise routing
and arbitrage on such networks as convex optimisation problems. We provide
bounds with closed formulas in the specific case of “constant product
” automated markets and a restricted form of cyclic arbitrage. We comput
e the associated lower bounds on actual data derived from the Ethereum blo
ckchain. (joint work with Hamza El Khalloufi and Julien Prat)\n\n\n\n[[htt
ps://zoom.us/meeting/register/tJIqc-qsrDIrHtPorBZ6znvrEr3AXkTjbSTG|Zoom re
gistration]]\n\n[[https://youtu.be/rNGvLt-w8nM|YouTube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Picturing Quantum Software - Aleks Kissinger\, Department of Compu
ter Science\, University of Oxford\, UK
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210716T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210716T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1411
DESCRIPTION:Quantum circuits give a de facto "assembly language" for quant
um computation. Hence\, the design\, optimisation\, and verification of qu
antum circuits is an important task in developing efficient\, correct soft
ware to run on quantum computers. In this talk\, I will survey some of the
latest developments in applying the ZX-calculus - a graphical theory of i
nteracting quantum processes - to three important problems in quantum soft
ware: the optimisation of quantum circuits\, functional verification of ci
rcuits\, and development of heuristics for efficient classical simulation.
\n\n\n[[https://zoom.us/meeting/register/tJUqce-hqz4vGtcHtQLLAVxbYgeHG8lna
FNN|Zoom registration]]\n\n[[https://youtu.be/G8uTHBMV918|YouTube live str
eam]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Logic of Hypergraphs - Filippo Bonchi\, Dipartimento di Inform
atica\, Università degli Studi di Pisa\, Italy
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210702T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210702T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1412
DESCRIPTION:A celebrated theorem of Chandra and Merlin states that Conjunc
tive Queries inclusion is decidable. Its proof transforms logical formulas
to hypergraphs: each query has a natural model – a kind of graph – an
d query inclusion reduces to the existence of a graph homomorphism between
natural models. In this talk\, we introduce the diagrammatic language Gra
phical Conjunctive Queries (GCQ) and show that it has the same expressivit
y as Conjunctive Queries. GCQ terms are string diagrams\, and their algebr
aic structure allows us to derive a sound and complete axiomatisation of q
uery inclusion\, which turns out to be exactly Carboni and Walters’ noti
on of cartesian bicategory of relations. Our completeness proof exploits t
he combinatorial nature of string diagrams as (certain cospans of) hypergr
aphs: Chandra and Merlin’s insights inspire a theorem that relates such
cospans with spans. Completeness and decidability of the (in)equational th
eory of GCQ follow as a corollary. Categorically speaking\, our contributi
on is a model-theoretic completeness theorem of free cartesian bicategorie
s (on a relational signature) for the category of sets and relations.\n\n\
n[[https://zoom.us/meeting/register/tJYsd-igpzsjH9zIsI6dyMdEjS3J68u3ShAs|Z
oom registration]]\n\n[[https://youtu.be/0t-VZqGV6UM|YouTube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Soundness for Automatic Differentiation via String Diagrams - Mari
o Alvarez-Picallo\, Department of Computer Science\, University of Oxford\
, UK
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210910T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210910T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1425
DESCRIPTION:Reverse-mode automatic differentiation\, especially in the pre
sence of complex language features\, is notoriously hard to implement corr
ectly\, and most implementations focus on differentiating straight-line im
perative first-order code. Generalisations exist\, however\, that can tack
le more advanced features\; for example\, the algorithm described by Pearl
mutter and Siskind in their 2008 paper can differentiate higher-order func
tions written in a pure functional language. We show that AD algorithms ca
n benefit enormously from being translated into the language of string dia
grams in two steps: first\, we describe a Pearlmutter-Siskind style AD alg
orithm as a set of rules for transforming hierarchical graphs\; rules whic
h can -and indeed have been- be implemented correctly and efficiently for
a non-trivial language. Then\, we present a proof of soundness for it by r
educing the above rewrite rules to a suitable graphical version of the axi
oms of Cartesian reverse differential categories\, expressed as string dia
grams.\n\n\n[[https://u-paris.zoom.us/meeting/register/tZckdu-opjIsGt2ZZJP
6eiPAATOM0ao3GAEZ|Zoom meeting registration link]]\n\n[[https://youtu.be/b
N7r6AbptwM|YouTube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Combinatorial maps: transformations and application to geometric m
odeling - Romain Pascual\, MICS laboratory\, CentraleSupélec\, University
Paris-Saclay\, France
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210924T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210924T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1426
DESCRIPTION:In the first part of the talk\, I will present generalized map
s that represent quasi-manifolds through their subdivision into topologica
l cells (vertices\,edges\, faces\, volumes). We defined generalized maps a
s constrained labeled graphs. Arc labels encode topological relations of t
he subparts modeled object while node labels describe the geometric data u
sed to represent the object. Modeling operations are designed regardless o
f the object's underlying topology. Therefore\, we generalize DPO rules wi
th a functorial approach to encode semi-global relabeling with a product o
peration. Rules and their extensions (called rule schemes) are considered
valid if any application to a well-formed graph results in an equally well
-formed graph. We provide set-theoric conditions on rules and rule schemes
to ensure the preservation of the model consistency. In the second part o
f the talk\, I will present how this approach allows the design of geometr
ic modelers (software used to create and edit geometric objects) in Jerboa
. The set-theoric conditions can be checked via graph traversal in Jerboa'
s rule editor to ensure that the code derived from the rule will never bre
ak the model. The generated code can be used as an add-on in other softwar
e or Jerboa's generic viewer. \n\n\n[[https://u-paris.zoom.us/meeting/reg
ister/tZUvd-igpj0qG9W_T2bsMKPEHInGUpmbkNqy|Zoom meeting registration link]
]\n\n[[https://youtu.be/woA2W-05fLQ|YouTube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Model Transformation Languages and Performance Engineering - Stefa
n Höppner & Raffaela Groner\, Institute of Software Engineering and Progr
amming Languages\, University of Ulm\, Germany
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211008T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211008T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1427
DESCRIPTION:This event will consist of two talks: "Investigating claimed A
dvantages and Disadvantages of Model Transformation Languages" (by Stefan
Höppner) and "Current State of Performance Engineering of Model Transform
ations" (by Raffaela Groner). Please refer to https://www.irif.fr/~greta/e
vent/2021-oct-08 for the respective abstracts.\n\n\n\n\n[[https://u-paris.
zoom.us/meeting/register/tZIkd-mrqjwiGdyHDYyjIo1bSCwpfBTNzNIe|Zoom meeting
registration link]]\n\n[[https://www.youtube.com/watch?v=LcoKDR4fSWw|YouT
ube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:GRAPEpress - A Computational Notebook for Graph Transformations -
Jens H. Weber\, Department of Computer Science\, University of Victoria\,
Canada
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211119T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211119T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1428
DESCRIPTION:Computational notebooks (CNs) have gained popularity in data s
cience\, artificial intelligence\, and engineering. CNs are used to docume
nt experiments and make them repeatable by incorporating executable segmen
ts and renderings of computational results. Unfortunately\, computations b
y graph transformations are not supported by current CNs. In order to clos
e this gap\, we have developed GRAPEPress\, a tool that combines the GRAPE
graph transformation language with the CN tool Gorilla. This talk introdu
ces the GRAPE language as well as its integration with the CN tool Gorilla
.\n\n\n\n\n[[https://u-paris.zoom.us/meeting/register/tZ0lfu-qpj0vHNGOI_uU
x3PwDpc3R5rNS5kS|Zoom meeting registration link]]\n\n[[https://www.youtube
.com/watch?v=zsAoz4Fbv_Q|YouTube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:GReTA-ExACT: towards Executable Applied Category Theory - Nicolas
Behr\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211105T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211105T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1486
DESCRIPTION:This talk marks the beginning of GReTA-ExACT\, a new online wo
rking group within the GReTA community. The aim of this working group will
consist in providing an interdisciplinary forum for exploring the diverse
aspects of applied category theory relevant in graph transformation syste
ms and their generalizations\, in developing a methodology for formalizing
diagrammatic proofs as relevant in rewriting theories via proof assistant
s such as Coq\, and in establishing a community-driven wiki system and rep
ository for mathematical knowledge in our research field (akin to a domain
-specific Coq-enabled variant of the nLab). A further research question wi
ll consist in exploring the possibility for deriving reference prototype i
mplementations of concrete rewriting systems (e.g.\, over multi- or simple
directed graphs) directly from the category-theoretical semantics\, in th
e spirit of the translation-based approaches as in [1]\,[2] (utilizing the
orem provers such as Microsoft Z3). \n\n\nIn the first part of this talk\,
I will provide an illustrated tour of broad scope of mathematical concept
s in modern categorical rewriting theories\, ranging over the definitions
of Double-Pushout (DPO) and Sesqui-Pushout (SqPO) semantics to the notions
of concurrency and associativity theorems\, their proofs (illustrating a
particular type of diagrammatic reasoning on commutative diagrams)\, the t
heory of tracelets\, their Hopf algebras and decomposition spaces\, certa
in concepts of opfibrations and finally double-categorical structures that
are currently under active investigation (joint work with Paul-André Mel
liès and Noam Zeilberger). In the second part of the talk\, I will outlin
e a proposal for the new GReTA-ExACT online working group format.\n\n\nRef
erences:\n\n[1] R. Heckel\, L. Lambers\, M.G. Saadat\, "Analysis of Graph
Transformation Systems: Native vs Translation-based Techniques"\, EPTCS 30
9\, 2019\, pp. 1-22. http://dx.doi.org/10.4204/EPTCS.309.1\n\n[2] N. Behr\
, R. Heckel\, M.G. Saadat\, "Efficient Computation of Graph Overlaps for R
ule Composition: Theory and Z3 Prototyping"\, EPTCS 330\, 2020\, pp. 126
–144. http://dx.doi.org/10.4204/EPTCS.330.8\n\n\n\n\n[[https://u-paris.z
oom.us/meeting/register/tZwrcuGoqT4qGd1HCZQnhptpmt0aTiWdDF67|Zoom meeting
registration link]]\n\n[[https://youtu.be/tx0asw82EXU|YouTube live stream]
]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:SMTCoq: the power of SMT solving in Coq - Chantal Keller\, Univers
ité Paris-Saclay\, CNRS\, ÉNS Paris-Saclay\, Laboratoire Méthodes Forme
lles\, Gif-sur-Yvette\, France
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211112T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211112T110000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1511
DESCRIPTION:[[https://smtcoq.github.io|SMTCoq]] is a tool to make the Coq
proof assistant and SMT solvers cooperate\, with the same degree of confid
ence as Coq. In this talk\, I will give an overview of its potential:\n\n*
checking SMT answers\, both in Coq and externally using the Coq extractio
n mechanism\n\n* importing SMT problems as Coq theorems\n\n* calling SMT s
olvers to ease Coq proof building\, in a ongoing project called [[https://
github.com/smtcoq/sniper|Sniper]].\n\n\n\nAn API to build first-order SMTC
oq terms and formulas is also under\nprogress\, in order to have an easy a
ccess to SMTCoq internal\nfunctionalities.\n\n\n\n\n[[https://u-paris.zoom
.us/meeting/register/tZwkfu2hrjsrGNWJvZSpbXXpnhOCiFOV5Y_3|Zoom meeting reg
istration link]]\n\n[[https://youtu.be/nc4x8EbL1oQ|YouTube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hierarchy Builder - Cyril Cohen\, Inria Sophia-Antipolis Méditerr
anée\, Sophia-Antipolis\, France
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211126T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211126T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1512
DESCRIPTION:Libraries of machine checked code are\, nowadays\, organized a
round hierarchies of algebraic structures. Unfortunately the language of T
ype Theory and the features provided by the Coq system make the constructi
on of a hierarchy hard even for expert users. The difficulty begins with t
he non-orthogonal choices\, between storing information as record fields o
r parameters\, and between using type classes and canonical structures for
inference. To this\, one may add the concerns about performance and about
the usability\, by a non expert\, of the final hierarchy. \n\nHB gives th
e library designer a language to describe the building blocks of algebraic
structures and to assemble them into a hierarchy. Similarly it provides t
he final user linguistic constructs to build instances (examples) of struc
tures and to teach the elaborator of Coq how to take advantage of this kno
wledge during type inference. Finally HB lets the library designer improve
the usability of his library by providing alternative interfaces to the p
rimitive ones\, a feature that can also be used to accommodate changes to
the hierarchy without breaking user code. \n\nThis is a joint work with Ka
zuhiko Sakaguchi and Enrico Tassi.\n\n\n\n\n[[https://u-paris.zoom.us/meet
ing/register/tZIqd-GgpjMtEtXUIhbc0Adinn7RXAqZbgH4|Zoom meeting registratio
n link]]\n\n[[https://youtu.be/nMynSM9Xnkw|YouTube live stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Formalizing Category Theory using Type Theory: A Discussion - Emil
io Jesús Gallego Arias\, Université de Paris\, CNRS\, IRIF\, France
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211210T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211210T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1513
DESCRIPTION:Since its inception at the start of the 20th century\, type th
eory has become a core foundational tool for those interested in the logic
al foundations of mathematics and computer science. A key milestone on the
field is the Calculus of Inductive Constructions\, the type theory that l
ies at the heart of modern interactive proof assistants such as Coq or Lea
n. The CiC is remarkably expressive\, yet remains computationally tractabl
e\, leading to important milestones in computer-checked mathematical resul
ts such as the 4 color theorem or the Feit-Thompson theorem. In this talk\
, we will present the calculus of inductive constructions as currently imp
lemented in the Coq proof assistant\, and we will explore the encoding of
basic constructions of category theory in Coq\, placing a particular empha
sis the usability and modularity of our definitions.\n\n\n\n\n[[https://u-
paris.zoom.us/meeting/register/tZwrdO2hrDssHtEB5TYi6tZPmm2hn1QCrspV|Zoom m
eeting registration link]]\n\n[[https://youtu.be/lM0b3oHDunU|YouTube live
stream]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Supporting Software Variability with Graph Transformations - Danie
l Strüber\, Department of Computer Science and Engineering\, Chalmers Uni
versity of Technology\, University of Gothenburg\, Sweden
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211203T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211203T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1517
DESCRIPTION:Software systems and the artifacts they consist of often exist
in many different variants. When creating new variants\, developers typic
ally rely on the "clone and own" strategy of copying and modifying existin
g variants\, a simple and intuitive approach with significant long-term di
sadvantages. In this talk\, I present a line of work on supporting variant
s in software engineering by explicitly addressing variability as a featur
e in graph transformations. I focus on three transformation scenarios: one
where the input graph has variability (representing the established notio
n of a software product line)\, one where rules have variability (leading
to variability-based rules)\, and a combination of the first two scenarios
. Each scenario is supported with formal constructions\, efficient transfo
rmation algorithms\, and tool support. Our work shows that a systematic wa
y of supporting variability in transformations can improve the maintainabi
lity and the performance of a software system.\n\n\n\n\n[[https://u-paris.
zoom.us/meeting/register/tZ0kcOqgrjsrHt2c7v0ElvEODTQn97b3RXU8|Zoom meeting
registration link]]\n\n[[https://youtu.be/8j0LHp7zGrE|YouTube live stream
]]
LOCATION:online
END:VEVENT
BEGIN:VEVENT
SUMMARY:Request-Guarantee Agents and their Check-Transform-Enforce Process
es - Paolo Bottoni\, Department of Computer Science\, Sapienza University
of Rome\, Italy
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20211217T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20211217T160000
DTSTAMP;VALUE=DATE-TIME:20211128T180302Z
UID:1521
DESCRIPTION:We introduce Check-Transfer-Enforce Systems (CTEs) as a genera
l model of behavior of (semi-)autonomous agents\, based on the idea of dis
tinguishing the ability of an agent to change its state from the actual ch
anges that can be performed under contextual constraints. In this model\,
based on many-sorted term algebras\, a Request-Guarantee (qg)-agent is cha
racterised by a collection of moves specifying which terms are requested t
o be present in the current state of the agents and which terms are guaran
teed to be present in the successor state\, if the move is executed. We sh
ow how this approach allows an encoding and a generalisation of a number o
f well-known existing models. The approach is naturally extended to the ca
se of pairs of communicating qg-agents. An abstract view of the approach c
an be given in the setting of enriched categories.\n\n\n\n[[https://u-pari
s.zoom.us/meeting/register/tZEkcOqsqDMuGNA5C0tn_piMtrGocFYI9g7p|Zoom meeti
ng registration link]]\n\n[[https://youtu.be/oTKwtGXApTo|YouTube live stre
am]]
LOCATION:online
END:VEVENT
END:VCALENDAR