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. 

