|
|
 |
|
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. |
Mardi 3 Mars
| 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 Les nombres et polynômes de Bernoulli sont des objets classiques qui apparaissent respectivement lors du prolongement analytique des fonctions zêta de Riemann et de Hurwitz aux entiers négatifs.En lien avec la généralisation multiple de ces fonctions, les multizêtas et multizêtas de Hurwitz, nous allons généraliser les nombres et polynômes de Bernoulli au cas multiple.Bien qu'il n'y a pas unicité d'une telle généralisation, nous introduirons un exemple explicite et satisfaisant où nombres de propriétés importantes des polynômes de Bernoulli se transmettent au cas multiple.Au passage, cela permet de répondre à une question sur la renormalisation des multizêtas aux entiers négatifs. |
Mercredi 4 Mars
| Heure: |
09:30 - 10:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
On an Extension of Freeze LTL with Ordered Attributes |
| Description: |
Normann Decker We present an extension of Freeze LTL, a temporal logic equipped with registers,
over data words. Each position in a (multi-attributed) data word carries a
letter from a finite alphabet and assigns a data value to a fixed, finite set of
attributes. While reasoning on collections of data values is valuable for
expressing correctness properties of executions of dynamic programs the
satisfiability problem of Freeze LTL is undecidable if more than one register is
available or tuples of data values can be stored and compared arbitrarily. Our
extension therefore allows for specifying a dependency relation on attributes.
These dependencies introduce a restricted, yet flexible way of storing and
comparing collections of attribute values. This new dimension of flexibility is
orthogonal to, e.g., the number of registers or the available temporal
operators. In this setting we characterise precisely the type of dependency
relations that maintain decidability of the logic. To this end, we employ
reductions from and to nested counter systems. Moreover, by a complexity
theoretic characterisations we can show that our extension is strict and induces
a semantic hierarchy of logical fragments. |
Vendredi 6 Mars
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
The Plotkin's call-by-value lambda-calculus from a linear-logical viewpoint |
| Description: |
Giulio Guerrieri We translate the terms of ordinary lambda-calculus into proof-nets
accordingly the Girard's call-by-value "boring'' encoding of intuitionistic
implication A->B = !A-o!B. We show that (1) the Plotkin's call-by-value
beta-reduction is (bi)simulated in proof-nets via cut-elimination; (2)
there is a sequentialization theorem that characterizes all and only the
proof-nets which are translations of some lambda-term; (3) the equivalence
relation on lambda-terms which identifies lambda-terms having the same
translation in proof-nets is the call-by-value counterpart of Regnier's
sigma-equivalence and is not included in Plotkin's call-by-value
beta-equivalence. The semantics of lambda-terms is preserved by our
call-by-value sigma-equivalence.
Adding an oriented version of the call-by-value sigma-rules to the
call-by-value beta-reduction (and keeping the same syntax of ordinary
lambda-calculus) we preserve confluence and we get a call-by-value
operational characterization of solvable and potential valuable terms (this
is not possible in original Plotkin's call-by-value lambda-calculus).
Moreover, we give a semantic characterization of solvable and potential
valuable terms in a relational model, based on Linear Logic, satisfying the
Taylor expansion formula. As a technical tool, we also use a
resource-sensitive calculus in which the elements of the model are
definable. |
|
|
