Lundi 1 Juillet
Heure: 
00:59  16:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
After the fscore: applying parser output in sentiment analysis, grammatical error detection and quality estimation for machine translation 
Description: 
Jennifer Foster several natural language processing applications, either because the&nbsp;"sensemaking" applications such as sentiment analysis or question&nbsp;in "language proofing" applications such as grammar checking or&nbsp;experiments carried out in the National Centre for Language Technology&nbsp;parser output in three downstream applications, namely, sentiment&nbsp;translation. In all these experiments some kind of phrase structure&nbsp;used to parse the input, and in some cases, the phrase structures were&nbsp;structure trees and dependency graphs was employed in the downstream&nbsp;clear from these experiments that syntactic parsing always provides some&nbsp;syntactic information or what the relationship between the accuracy of&nbsp;F1 or labelled attachment accuracy) and its usefulness in the downstream&nbsp; 
Vendredi 5 Juillet
Heure: 
00:59  14:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Forcing in classical realizability: the case study of Herbrand trees 
Description: 
Lionel Rieg Krivine presented in 2010 a methodology to combine Cohen's forcing with the theory of classical realizability and showed that the forcing condition can be seen as a reference that is not subject to backtracks. The underlying classical program transformation was then analyzed by Miquel (2011) in a fully typed setting in classical higherorder arithmetic (PAw+).As a case study of this methodology, I present a method to extract a Herbrand tree from a classical realizer of an existential formula, following the idea of the proof of Herbrand theorem.&nbsp; Unlike the traditional proof based on Konig's lemma (using a fixed enumeration of atomic formulas), our method is based on the introduction of a particular Cohen real.&nbsp; It is formalized as a proof in PAw+, making explicit the construction of generic sets in this framework in the particular case where the set of forcing conditions is arithmetical.&nbsp; We then analyze the algorithmic content of this proof. 
Mercredi 10 Juillet
Heure: 
13:30  16:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Soutenance à miparcours 
Description: 
Nguyen HoangNghia 
Heure: 
14:30  17:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Soutenance à miparcours 
Description: 
Ladji Kane 
Heure: 
15:30  18:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Soutenance à miparcours 
Description: 
Alice Jacquot 
Heure: 
16:30  19:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Goûter de clôture 
Vendredi 12 Juillet
Heure: 
00:59  12:00 
Lieu: 
Amphi Copernic, Institut Galilée, Université de Villetaneuse 
Résumé: 
Bisimulations from graphical encodings (DPOs, RPOs, cospans, and all that) 
Description: 
Fabio Gadducci The talk presents a personal recollection of recent results on the synthesis of labelled transition systems (LTSs) for process calculi. The starting point is a visual technique for modelling the reduction semantics of nominal calculi: processes are mapped into graphs equipped with "interfaces", such that the denotation is fully abstract with respect to the structural congruence. The encoding allows for the reuse of standard graph rewriting theory and tools for simulating the reduction semantics of the calculus, such as the "double pushout" (DPO) approach and its concurrent semantics (which allows for the simultaneous execution of independent reductions) Graphs with interfaces are just an instance of a cospan category (over the category of graphs). which is amenable to the synthesis mechanism based on "borrowed contexts" (BCs), proposed by Ehrig and Koenig, which are in turn an instance of "relative push outs" (RPOs), originally introduced by Milner and Leifer. The BC mechanism allows for the effective construction of an LTS that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. Since the category of cospans over graphs admits RPOs (as proved by Sassone and Sobocinski), its choice as the domain of the encoding for nominal calculi ensures that the synthesis of an LTS can be performed, and that a compositional observational equivalence is obtained. The talk discusses the LTS distilled by exploiting the encoding of CCS and Mobile Ambients processes. 

