2015


Retour à la vue des calendrier
Mardi 6 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Généralisation des nombres et polynômes de Bernoulli aux cas multiples
Description: Olivier Bouillot
Mercredi 7 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Generalized paper-folding sequences
Description: Johan Nilsson
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Extracting information from text: Language Understanding and Sentiment analysis
Description: Emilio Sanchis
Mardi 13 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Generalized paper-folding sequences
Description: Johan Nilsson
Mercredi 14 Janvier
Heure: 15:30 - 16:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Cost Linear Temporal Logic for Verification
Description: Maximilien Colange Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton.
The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton.
This method can be extended with various automata flavors to handle quantitative properties.

We focus on an extension of Linear Temporal Logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL).
This logics can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking.
We describe the new properties that this extension allows to handle, illustrated with examples.
We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses.
We also propose a CEGAR-like approach to answer compute the bounds of the values reached by the automata.
Vendredi 16 Janvier
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Approche philologique des langages de programmation
Description: Baptiste Mélès La théorie des langages de programmation s'appuie généralement sur des langages de programmation théoriques — lambda-calcul, machines de Turing, et leurs variantes — que l'on suppose représenter fidèlement — à compilation près ! — les propriétés des langages de programmation de la « vraie vie », si l'on entend par là ceux que les programmeurs utilisent pour écrire des programmes utiles au quotidien : C, C++, Perl, etc.

Or nous allons voir que les langages de programmation de la vraie vie possèdent bien des propriétés dont nul ne voudrait dans un langage théorique, et que la compilation écrase : des commandes inutiles, des redondances, des résidus purement historiques... Qui plus est, loin d'être un fait simplement négatif, ces propriétés constituent une bonne part de leur expressivité du point de vue du programmeur, et sont autant de points communs avec les langues naturelles. Nous verrons ainsi que des outils linguistiques et philologiques peuvent être mobilisés pour décrire une « sémantique du programmeur », qui échappe pour une bonne part aussi bien aux sémantiques courantes des langages de programmation qu'aux tentatives de description formelle de l'expressivité des langages de programmation.
Lundi 19 Janvier
Heure: 13:30 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: A Text Analytic Approach to Historical Legal Records
Description: Adam Zachary Wyner The council registers of Aberdeen, Scotland are the earliest and most complete body of town (or burgh) council records in Scotland, running nearly continuously from 1398 to the present; they are hand written in Latin and (largely) Middle Scots. Few cities in the United Kingdom or in Western Europe rival Aberdeen's burgh registers in historical depth and completeness. In July 2013, UNESCO UK recognised the register volumes from 1398 to 1509 as being of outstanding historical importance to the UK. The registers offer a detailed view into the legal aspects of life in one of Scotland's principal burghs, providing a view into administrative, legal, and commercial activities as well as daily life. The registers include information about a range of matters, from the elections of office bearers, property transfers, regulations of trade and prices, references to crimes and subsequent punishment, to matters of public health, credit and debt, cargoes of foreign vessels, tax and rental o
f burgh lands, and woods and fishings. Thus the entries present the burgh's relationships with the countryside and countries around the North Sea.

This talk discusses the results of a text analytic project developed around 100 transcribed pages of these records from the period 1530-1531. We worked with the General Architecture for Text Engineering (GATE) text analytic tool. In the project, we created a large, rich, and varied range of semantic annotations such as individual's names, locations, various materials of trade, legal concepts, translation, offices, social status, documents, shipping terminology, and many others. The annotations can be examined either in situ or as complex semantic queries.

With this application, users can hover over the text and receive a translation into English, making the text accessible to a large audience. Legal historians can query and study the text in novel and illuminating ways, for example, rapidly examining the use of particular terminology or patterns over the whole corpus. Moreover, legal historians can scale up their textual studies - while the particular tool was developed for only 100 pages, it can be applied to larger corpus of related material of some 600 pages. The tool is also highly extensible, allowing for modification of the current analysis as well as the addition of other material that may be beyond the scope of the Aberdeen registers.

We outline the project objectives, present the text analytic tool, show the range of annotations, provide some sample results of queries, relate our work to other projects, and sketch future work. Broadly, the paper and project contribute to the application of language technologies for cultural heritage and the humanities. More specifically, the research provides a text analytic approach to studying the evolution of legal concepts and their application over time, providing legal historians with the means to gain fresh insights to historical and contemporary legal systems.
Mardi 20 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Statistical physics and combinatorics
Description: Francesco Caltagirone
Mercredi 21 Janvier
Heure: 14:00 - 15:00
Lieu: Amphi A
Résumé: Quantum Computing: From physics to computational systems
Description: Andrea Masini
Jeudi 22 Janvier
Heure: 16:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Specification and verification of Time Petri Nets with Coq
Description: Amal Chamakh Model checking and theorem proving, have long reached their limitation as
general-purpose techniques, and most of the research now is concentrated on
efficient specialization of both approaches to relatively narrow problem
domains. The state space explosion problem leaves little hope for automatic
finite-state verification techniques like model checking to remain
practical, especially when designs become parameterized. The use of theorem
proving techniques is inevitable to cope with the new verification
challenges. "Pure" theorem proving, on the other hand, can also be quite
tedious and impractical for complex designs. Ideally, one would like to
find an efficient combination of model checking and theorem proving, and
the quest for such a combination has long been one of the major challenges
in the field of formal verification. In this paper, we address the
combination of model checking and theorem proving approaches in order to
specify and to model check Time Petri Nets (TPN) model-based systems. In
particular, we show how a TPN is specified using the Coq proof assistant,
and how the fireability/unfireability of a timed sequence of transitions
can be proved. This allows, for instance, to prove the reachability of a
given state by the firing of a given timed/untimed trace or to prove that a
counter-example supplied by a given (untimed) model checker is a real
counterexample of a timed system. %First, we provide a formalization of the
net model in COQ via the parsing of its Petri Net Markup Language (PNML)
description. Then the COQ proof assistant is used to prove the firability
(or the opposite) of traces given by model checking as a counter-example
when a propriety being checked is found to be non-valid, hence, states
reachability is proved.
Vendredi 23 Janvier
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: An Introduction to Higher-Dimensional Rewriting Theory
Description: Samuel Mimram À venir.
Lundi 26 Janvier
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Apprentissage faiblement supervise d'un etiqueteur morpho-syntaxique par transfert cross-lingue
Description: Guillaume Wisniewski Les méthodes de transfert cross-lingue permettent
partiellement de pallier l'absence de corpus annotés, en particulier
dans le cas de langues peu dotées en ressources linguistiques. Le
transfert d'étiquettes morpho-syntaxiques depuis une langue riche en
ressources, complété et corrigé par un dictionnaire associant à
chaque mot un ensemble d'étiquettes autorisées, ne fournit cependant
qu'une information de supervision incomplète. Dans ce travail, nous
reformulons ce problème dans le cadre de l'apprentissage
ambigu et proposons une nouvelle méthode pour apprendre un
analyseur de manière faiblement supervisée à partir d'un modèle à
base d'historique. L'évaluation de cette approche montre une amélioration
sensible des performances par rapport aux méthodes de l'état de
l'art.
Mardi 27 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Soutenance de thèse (AOC-RCLN)
Description: Nada Mimouni
Vendredi 30 Janvier
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Une introduction à la théorie de Squier
Description: Yves Guiraud Un monoïde ayant une présentation par un système de réécriture convergent
fini a un problème du mot décidable. Dans les années 1980, Jantzen
s'interroge sur la réciproque : un monoïde ayant un problème du mot
décidable admet-il toujours une présentation par un système de réécriture
convergent fini ? Squier a répondu négativement à cette question en reliant
des propriétés algorithmiques des systèmes de réécriture, comme la
terminaison et la confluence, à des invariants algébriques, comme
l'homologie ou l'homotopie.

Dans cet exposé, je présenterai le résultat initial de Squier, dans le
formalisme de la réécriture de dimension supérieure. Puis, nous verrons
comment le travail de Squier permet aujourd'hui d'utiliser la réécriture
comme méthode constructive pour calculer des invariants de structures
algébriques.
Heure: 14:00 - 14:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Cost Linear Temporal Logic for Verification
Description: Maximilien Colange Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton. This method can be extended with various automata flavors to handle quantitative properties.

We focus on an extension of Linear Temporal Logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL). This logics can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking. We describe the new properties that this extension allows to handle, illustrated with examples. We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses. We also propose a CEGAR-like approach to answer compute the bounds of the values reached by the automata.
Heure: 14:40 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Vérification de Spécifications EB-3 à l'aide de Techniques de Model Checking
Description: Dimitrio Vekris EB-3 est un langage de spécification développé pour la spécification des systèmes d'information. Le noyau du langage EB-3 comprend des spécifications d'algèbre de processus afin de décrire le comportement des entités du système et des fonctions d'attributs qui sont des fonctions récursives dont l'évaluation se fait sur la trace d'exécution du système décrivant les attributs des entités. La vérification de propriétés temporelles en EB-3 est un sujet de grande importance pour des utilisateurs de EB-3. Dans cet exposé, on se focalise sur les propriétés de vivacité concernant des systèmes d'information exprimant l'éventualité que certaines actions puissent s'exécuter. La vérification des propriétés de vivacité se fait à l'aide de model checking.

En se basant sur une sémantique opérationnelle de EB-3, selon laquelle les fonctions d'attributs sont évaluées pendant l'exécution du programme puis stockées, on définit une traduction automatique de EB-3 vers LNT, qui est un langage simultané enrichi d'une algèbre de processus. Notre traduction assure la correspondance un à un entre les états et les transitions des systèmes étiquetés de transition correspondent respectivement à des spécifications EB-3 et LNT. Ensuite, on automatise la traduction grâce à l'outil EB3toLNT fournissant aux utilisateurs de EB-3 tous les outils de vérification fonctionnelle disponible dans CADP.
Mardi 3 Février
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Graph polynomials and relations with physics
Description: Adrian Tanasa In the first part of the talk I will introduce the Tuttepolynomial of graphs and explicitly show its relation withpolynomials appearing in the so-called parametric representation ofintegrands canonically associated to graphs in quantum field theory.In the second part of the talk I will show a new proof of thecelebrated property of universality of the Tutte polynomial of graphs(or matroids), proof which does not require the usual edge inductionarguments. Finally, I will present how this proof generalizes for theuniversality property of the Bollobas-Riordan polynomial of ribbongraphs (or embedded graphs).
Mardi 10 Février
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Énumérer les cartes farcies de toute topologie (avec un soupçon de combinatoire analytique)
Description: Gaëtan Borot Les cartes sont des surfaces discrètes construites en recollant lelong de leurs bords des polygônes - l'exemple le plus simple étant lestriangulations. En tant que surfaces orientables, leur topologie estcaractérisée par le nombre de bords n, et le nombre d'anses g. Si l'onse donne un poids de Boltzmann t_k pour chaque k-gone, l'énumérationdes cartes à un bord et de genre 0 est un problème très bien étudié.Ici, je considèrerai le problème plus général d'énumérer les cartesfarcies: ce sont les surfaces obtenues en a) piochant dans une boîte àoutils pouvant contenir des surfaces à bords polygonaux et detopologie quelconque ; b) en recollant ces morceaux élémentaires lelong de leurs bords ; c) pondérant l'énumération par des poids deBoltzmann dépendant du genre et de la longueur des bords de chaquemorceau élémentaire. J'expliquerai notamment qu'il existe unerécurrence universelle sur la caractéristique d'Euler totale 2 - 2g -n, qui réduit le problème d'énumération en toute topologie à celui desdisques (n = 1, g = 0) et des cylindres (n = 2,g = 0).
Vendredi 13 Février
Heure: 11:30 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Model checking en logique de dépendance
Description: Nicolas de Rugy-Altherre La logique de dépendance et ses variantes (indépendance et inclusion) ont été introduites par Vänäänen il y a quelques années pour parler de façon "propre" de dépendance en logique. Je présenterai cette logique et ses résultats principaux en complexité.
Mardi 17 Février
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Problèmes de satisfaction de contraintes et graphes inhomogènes
Description: Élie de Panafieu
Jeudi 19 Février
Heure: 16:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Modelling Timed Concurrent Systems Using Activity Diagram Patterns
Description: Étienne André UML is the de facto standard for modelling concurrent systems in the industry.
Activity diagrams allow designers to model workflows or business processes.
Unfortunately, their informal semantics prevents the use of automated verification techniques.
In this paper,
we first propose activity diagram patterns for modelling timed concurrent systems;
we then devise a modular mechanism to compose timed diagram fragments into a UML activity diagram that also allows for refinement, and
we formalise the semantics of our patterns using time Petri nets.
Our approach guides the modeller task% (helping to avoid common mistakes), and allows for automated verification.

Joint work with Christine Choppy and Thierry Noulamo
Vendredi 20 Février
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Coherence spaces for computable analysis
Description: Kazushige Terui Abstract:
There have been two mainstream approaches in
computable analysis: the type-two theory of effectivity (TTE)
and the theory of domain representations. This paper proposes
an intermediary approach based on coherence spaces, which is
as concrete as TTE and as structured as domain theory.

We import various concepts from TTE such as admissibility,
and provide admissible representations for the real line, Euclidean
spaces and function spaces over them. This allows us
to represent, for instance, a real continuous function by a stable
map. A natural question is then what linear maps correspond
to in terms of analysis. Our answer is that they correspond
to uniformly continuous functions. This leads to an internal
expression of Heine's theorem (every continuous function on a
compact interval of the real line is uniformly continuous) as the
existence of a certain map from a stable function space to a linear
function space.

We finally illustrate an application of coherence spaces as a
type system for lambda calculus, which allows us to verify local
properties of real functions.

This is a joint work with Kei Matsumoto.
Mardi 24 Février
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Profile of random trees
Description: Michael Drmota
Mercredi 25 Février
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Quasi-random properties of subsequences of sequences generated by finite automata
Description: Michael Drmota Automatic sequences T(n) are the output sequence of a finite automaton, wherethe input is the q-adic digital representation of n. The most prominent exampleis the Thue-Morse sequence t(n) (that is also the fixed point of the substitution0 -> 01, 1 -> 10). Automatic sequences have been studied in many diff erent contextsfrom combinatorics to algebra, number theory, harmonic analysis, geometryand dynamical systems. For example, they have a linear subword complexity andthey are almost periodic.Since the subword complexity is linear the entropy of the related dynamical system is zero. This also means thatthey do not behave like a random sequence. However, the situation changes drastically whenone uses proper subsequences of automatic sequences, for example the subsequence along primes orsquares. It is conjectured that the resulting sequences are normal sequences so thatthey behave like random sequences (=quasi random sequences).Recently this property was proved (together with C. Mauduit and J. Rivat)for the Thue-Morse sequence along the subsequence of squares - and it turns out that thispropery extends to several other automatic sequences and also to subsequences of the form[n^c], where 1 < c < 4/3. Thus such subsequences of automatic sequences give rise toa completely new class of pseudo random sequences that can be computed very efficiently.
Heure: 14:00 - 15:00
Lieu: Amphi A
Résumé: Quasi-Random Properties of Subsequences of Sequences Generated by Finite Automata
Description: Michael Drmota Automatic sequences T(n) are the output sequence of a finite automaton, where
the input is the q-adic digital representation of n. The most prominent example
is the Thue-Morse sequence t(n) (that is also the fixed point of the substitution
0 -> 01, 1 -> 10). Automatic sequences have been studied in many diff erent contexts
from combinatorics to algebra, number theory, harmonic analysis, geometry
and dynamical systems. For example, they have a linear subword complexity and
they are almost periodic.

Since the subword complexity is linear the entropy of the related dynamical system is zero. This also means that
they do not behave like a random sequence. However, the situation changes drastically when
one uses proper subsequences of automatic sequences, for example the subsequence along primes or
squares. It is conjectured that the resulting sequences are normal sequences so that
they behave like random sequences (=quasi random sequences).
Recently this property was proved (together with C. Mauduit and J. Rivat)
for the Thue-Morse sequence along the subsequence of squares - and it turns out that this
propery extends to several other automatic sequences and also to subsequences of the form
[n^c], where 1 < c < 4/3. Thus such subsequences of automatic sequences give rise to
a completely new class of pseudo random sequences that can be computed very efficiently.
Vendredi 27 Février
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Linear numeral systems
Description: Ian Mackie We take a fresh look at an old problem of representing natural numbers
in the lambda-calculus. Our interest is in finding representations
where we can compute efficiently (and where possible, in constant
time) the following functions: successor, predecessor, addition,
subtraction and test for zero. Surprisingly, we find a solution in the
linear lambda-calculus, where copying and erasing are not permitted.
Lundi 2 Mars
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Open questions on Dynamic Semantic Annotation
Description: Ivan GARRIDO MARQUEZ Semantic annotation provides a powerful advantage for several
applications requiring text analysis. Semantic annotation requires the
presence of a semantic model to link the elements of the text to their
semantic representation. An a priori built ontology requires to be
maintained, adapted and to grow to keep its usefulness. When this update
is made along the annotation process, by exploiting the annotated text
to enrich the model we can discuss a dynamicity of the annotation. We
can identify two processes closely related with this dynamicity, the
knowledge acquisition and the annotation process itself. On this talk we
will try present an overview on this processes and how they have been
approached before.