Seminars

Invalid Start Date
start 7180325
Links' Seminars and Public Events Add to google calendar
2016
Thu 21st Jan
11:00 am
1:00 pm
Add event to google
Seminar by Vincent Penelle: "Rewriting high-order stack trees"
Higher-order pushdown systems and ground tree rewriting systems can
be seen as extensions of suffix word rewriting systems. Both classes
generate infinite graphs with interesting logical
properties. Indeed, the satisfaction of any formula written in
monadic second order logic (respectively first order logic with
reachability predicates) can be decided on such a graph.

The purpose of this talk is to propose a common extension to both
higher-order stack operations and ground tree rewriting. We introduce a model
of higher-order ground tree rewriting over trees labelled by
higher-order stacks (henceforth called stack trees), which syntactically
coincides with ordinary ground tree rewriting at order 1 and with the dynamics
of higher-order pushdown automata over unary trees. The infinite
graphs generated by this class have a decidable first order logic with
reachability.

Formally, an order n stack tree is a tree labelled by order n-1 stacks.
Operations of ground stack tree rewriting are represented by a certain class
of connected DAGs labelled by a set of basic operations over stack trees
describing of the relative application positions of the basic
operations appearing on it. Applying a DAG to a stack tree t intuitively
amounts to paste its input vertices to some leaves of t and to simplify
the obtained structure, applying the basic operations labelling the edges of the
DAG to the leaves they are appended to, until either a new stack tree is
obtained or the process fails, in which case the application of the DAG to t
at the chosen position is deemed impossible. This model is a common extension
to those of higher-order stack operations presented by Carayol and of ground tree
transducers presented by Dauchet and Tison.

As further results we can define a notion of recognisable sets of
operations through a generalisation. The proof that the graphs generated
by a ground stack tree rewriting system have a decidable first order theory
with reachability is inspired by the technique of finite set interpretations
presented by Colcombet and Loding.
"Lille-Salle B21"
Thu 14th Jan
 all day
Add event to google
visite pierre senellart
Tue 12th Jan
to Thu 14th Jan
 all day
Add event to google
visite Antoine Amarilli
2015
Mon 14th Dec
2:00 pm
4:00 pm
Add event to google
Slawek Staworko's HDR defense: "Symbolic Inference Methods for Databases"

Show in Google map
M2, salle de réunion
Fri 20th Nov
10:30 am
12:30 pm
Add event to google
Seminar Links by Stéphane Demri: "Separation Logic and Friends"
Abstract: Separation logic is used as an assertion language for
Hoare-style proof systems about programs with pointers,
and there is an ongoing quest for understanding its
complexity and expressive power. There are also
a lot of activities to develop verification methods
with decision procedures for fragments of practical use.

Actually, there exist many variants for separation
logic that can be viewed as fragments of second-order logic,
as well as variants of modal or temporal logics in which
models can be updated dynamically.

In this talk, after introducing first principles on separation logic,
issues related to decidability, computational complexity and expressive
power are discussed. We provide several tight relationships with
second-order logics, interval temporal logics or data logics, depending
on the variants of the logic and on the syntactic resources available.
"Lille-Salle B21"
Fri 13th Nov
10:30 am
12:00 pm
Add event to google
Seminar Links by Iovka Boneva: "Shape Expressions Schemas"
Abstract:
Shape Expressions Schemas is an expressive schema and constraint language for RDF data. I am going to define the language, illustrate it with examples, then give a validation algorithm and talk about ongoing work.
"Lille-Salle B21"
Thu 29th Oct
10:00 am
12:00 pm
Add event to google
Seminar Links by Antoine Amarilli
"Lille-Salle A11"
Fri 9th Oct
10:30 am
12:30 pm
Add event to google
Seminar Links: Adrien Boiret

"Lille-Salle B21"
Thu 1st Oct
10:30 am
12:30 pm
Add event to google
Seminar Links by Eric Prud'hommeaux: Shape Expressions: (finally) a schema language for RDF graph structure
Initial architects envinsioned RDF as a knowledge representation language, freeing users from syntactic limitations and revolutionizing the way information was exchanged.
While inference and description logic are applied to RDF, the foundation of simple assertions composed of global, unambiguous identifiers, has many more mondane and practical applications.
Distributed contributions to large (web-scale) data graphs demands adaptation of tree and stream-based validation techniques to operate over a graph.
Shape Expressions performs an ordered traversal of RDF graphs to
1 validate of structural constraints.
2 perform generative semantic actions.
"Lille-Salle B21"
Fri 11th Sep
12:00 pm
1:00 pm
Add event to google
Florent Capelli

Permanent link to this article: https://team.inria.fr/links/seminars/