Seminars

Links' Seminars and Public Events Add to google calendar
2017
Mon 9th Jan
to Fri 13th Jan
 all day
Add event to google
Visite Michael vanden Boom, Oxford University
2016
Fri 9th Dec
 all day
Add event to google
Kickoff Headwork
Show in Google map
Paris MNHN
Fri 18th Nov
10:30 am
12:00 pm
Add event to google
Florent Capelli Links Seminar
"Lille-Salle B21"
Fri 18th Nov
 all day
Add event to google
Florent Capelli visit
Tue 8th Nov
2:30 pm
4:30 pm
Add event to google
Seminar Link by Helmut Seidl: "Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable"
Abstract:

We show that equivalence of deterministic top-down tree-to-string transducers is decidable,
thus solving a long standing open problem in formal language theory.
We also present efficient algorithms for subclasses:
polynomial time for total transducers with unary output alphabet (over a given top-down regular domain language),
and co-randomized polynomial time for linear transducers, these results are obtained using techniques from multi-linear algebra.
For our main result, we prove that equivalence can be certified by means of inductive invariants using polynomial ideals.
This allows us to construct two semi-algorithms, one searching for a proof of equivalence, one for a witness of non-equivalence.
"Lille-Salle B31 "
Mon 7th Nov
2:00 pm
4:00 pm
Add event to google
PhD defense Adrien Boiret
Fri 4th Nov
 all day
Add event to google
colis general meeting
Show in Google map
Paris
Thu 27th Oct
10:00 am
6:00 pm
Add event to google
Links day
Thu 27th Oct
 all day
Add event to google
links day
Thu 20th Oct
2:00 pm
4:00 pm
Add event to google
Seminar Links by Vincent Hugot: "Top-Down Transducers for Data Trees"
Abstract:
Tree transducers have a wide range of application domains ranging from compiler construction,
program analysis, and computational linguistics, to semi-structured databases and file system
transformations. A common application of these domains is to specify and verify transformations
of data trees, i.e., trees whose nodes are labeled by data values from an infinite domain. Most
existing classes of tree transducers and their formal studies, however, are restricted to trees over
finite signatures without data. In this paper, we lift the most prominent class of top-down tree
transducers to data trees, such that its good properties are preserved. In particular, we show that
top-down transducers for data trees have a decidable equivalence problem, without imposing any
linearity restriction as in previous approaches based on symbolic top-down tree transducers.
"Lille-Salle B21"
Thu 13th Oct
2:00 pm
3:00 pm
Add event to google
Seminar Christof Löding
"Lille-Salle B21"
Thu 13th Oct
2:00 pm
5:30 pm
Add event to google
comité de projet
Thu 13th Oct
to Fri 14th Oct
 all day
Add event to google
visit christof löding
Fri 30th Sep
 all day
Add event to google
arrivée de Jose Lozano

Thu 29th Sep
2:00 pm
4:00 pm
Add event to google
Seminar Links by Aurélien Lemay

"Lille-Salle B21"
Tue 27th Sep
 all day
Add event to google
Ircica fetes ces 10 ans
Show in Google map
Lille
Fri 9th Sep
2:00 pm
4:00 pm
Add event to google
Momar Sakho
"Lille-Salle B21"
Wed 7th Sep
11:00 am
12:00 pm
Add event to google
jason demagoj
Wed 31st Aug
10:00 am
1:00 pm
Add event to google
Links Seminar by Domagoj Vrgoč: "Querying Graph with Data"
"Lille-Salle B21"
Thu 28th Jul
 all day
Add event to google
Visit of Serge Abiteboul and Victor Vianu
Mon 11th Jul
to Tue 12th Jul
 all day
Add event to google
Aggreg meeting
Show in Google map
Marseille
Mon 27th Jun
 all day
Add event to google
Colis ANR project: general meeting
Show in Google map
Inria Paris, Salle 119 "Ada Lovelace"
Fri 24th Jun
2:00 pm
4:00 pm
Add event to google
Fatima Belkouch: on the hypercube algorithm for conjunctive queries
Abstract: We consider the problem of computing a conjunctive query on a large database in a parallel setting with p servers. Unlike traditional query processing, the complexity is no longer dominated by the number of disk accesses. Typically, a query is evaluated by a sufficiently large number of servers such that the entire data can be kept in the main memory of these servers. The dominant cost becomes that of communicating data and synchronizing among the servers.
I will present some interesting results in [1, 2, 3, 4] dealing with the communication complexity of massively parallel computation of a query. The computation is performed in "rounds".
First, I will present the Massively Parallel Communication (MPC) model to analyze the tradeoff between the number of rounds and the amount of communication required in a massively parallel computing environment.
Then I will present the HyperCube (HC) algorithm that computes a full conjunctive query q in one round.
I will discuss the communication complexity [2]. The main result is the optimal load O(m/p1/τ ) where τ is the fractional vertex cover of the hypergraph of q and m the input data size.

References
[1] Parallel Evaluation of Conjunctive Queries. Paris Koutris, Dan Suciu PODS2011
[2] Communication Steps for Parallel Query Processing. Paul Beame, Paris Koutris, Dan Suciu PODS2013
[3] Skew in Parallel Query Processing. Paul Beame, Paris Koutris Dan Suciu PODS'2014
[4] Worst-Case Optimal Algorithms for Parallel Query Processing. Paris Koutris, Paul Beame, Dan Suciu ICDT2016
"Lille-Salle B11"
Thu 23rd Jun
2:00 pm
3:30 pm
Add event to google
Victor Vianu in Polaris
Show in Google map
Auditorium IRCICA
Thu 23rd Jun
 all day
Add event to google
victor vianu visit
Mon 20th Jun
to Wed 22nd Jun
 all day
Add event to google
journee scientique inria à rennes
Fri 17th Jun
9:00 am
12:30 pm
Add event to google
PhD Thesis Defense by Tom Sebastian: Evaluation of XPath Queries on XML streams with Networks of Early Nested Word Automata

Abstract:
The challenge that we tackle in this thesis is the problem of how to answer
XPath queries on XML streams with low latency, full coverage, high time
efficiency, and low memory costs. We first propose to approximate earli-
est query answering for navigational XPath queries by compilation to early
nested word automata. It turns out that this leads to almost optimal la-
tency and memory consumption. Second, we contribute a formal semantics
of XPath 3.0. It is obtained by mapping XPath to the new query language
λXP that we introduce. We then show how to compile λXP queries to net-
works of early nested word automata, and develop streaming algorithms for
the latter. Thereby we obtain a streaming algorithm that indeed covers all of
XPath 3.0. Third, we develop an algorithm for projecting XML streams with
respect to the query defined by an early nested word automaton. Thereby
we are able to make our streaming algorithms highly time efficient. We have
implemented all our algorithms with the objective to obtain an industrially
applicable streaming tool. It turns out that our algorithms outperform all
previous approaches in time efficiency, coverage, and latency.
Thu 16th Jun
2:00 pm
4:00 pm
Add event to google
Nicolas Bacquey Links seminar: Introduction to uniform periodical computation : leader election on periodical cellular automata
"Lille-Salle B21"
Thu 16th Jun
10:00 am
12:00 pm
Add event to google
Hubie Chen, Semainar and Visit
"Lille-Salle B21"
Fri 22nd Apr
10:00 am
11:30 am
Add event to google
Assemblée générale Inria Lille
Fri 1st Apr
 all day
Add event to google
Laurent d'Orazio (cancelled)
Fri 25th Mar
 all day
Add event to google
Datacert ANR project: general meeting
Show in Google map
Lyon
Fri 18th Mar
10:30 am
12:00 pm
Add event to google
Charles Paperman: "Streaming and circuit complexity"
Abstract:
In this talk, I will present a connection between the streaming complexity and the circuit complexity of regular languages through a notion of streaming by block . This result provides tight constructions of boolean circuits computing an automaton, thanks to some classical and recent results on the circuit complexity of regular languages. I will apply this framework to the schema validation in streaming of XML-documents.
Show in Google map
Inria Lille
Fri 18th Mar
 all day
Add event to google
Visit of Charles Paperman, Université Paris 7
Show in Google map
Inria Lille
Fri 11th Mar
10:30 am
12:00 pm
Add event to google
Seminar Links by Sylvain Salvati: Behavioral verification of higher-order programs
Abstract: Higher-order constructions make their way into main stream
programming languages like Java, C++, python, rust... These
constructions bring new challenges to the verification of programs as
they make their control flow more complex.

In this talk, I will present how methods coming from denotational
semantics can prove decidable the verification of certain properties of
higher-order programs. These properties are expressed by means of finite
state automata of the possibly infinite execution trees generated by the
programs and can capture safety properties but also liveness and
fairness properties.
Fri 11th Mar
 all day
Add event to google
Sylvain Salvati: visit and Talk
Université Bordeaux 1

www.labri.fr/perso/salvati
Wed 9th Mar
1:30 pm
2:00 pm
Add event to google
cristan duriez 30 minutes de science inria lille
Fri 4th Mar
 all day
Add event to google
Colis ANR project: general meeting
Show in Google map
Inria Lille, Salle B21
Thu 3rd Mar
 all day
Add event to google
Kim Nguyen: visit for discussion with Links' members (no talk)
Université Paris Sud
www.lri.fr/~kn/
Show in Google map
B218
Fri 19th Feb
11:00 am
3:00 pm
Add event to google
CNRS, Université Lens
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/