Dès les débuts de l’informatique, la linguistique a été à la fois un champ d’investigation privilégié (traduction automatique) et la source de notions clefs (la théorie des langages formels). Plus récemment la logique est apparue comme un élément fédérateur capable de traiter de la sémantique de la langue, mais aussi de sa syntaxe. L’équipe SIGNES souhaite réaliser et articuler les modèles et algorithmes correspondant aux différents niveaux d’étude et de traitement informatique de la langue, l’accent étant placé sur l’interface entre syntaxe et sémantique.
Plus précisément, elle se propose de modéliser par des méthodes formelles :
 théorie des langages
 grammaires catégorielles
 logique des ressources
 lambda-calcul
 logique d’ordre supérieur

certains aspects de la langue :
 morphologie dérivationnelle et sémantique lexicale
 morphologie flexionnelle
 prosodie
 syntaxe
 sémantique logique
 représentation du discours

Parmi les objectifs envisagés, il faut mentionner le lien entre grammaires formelles et grammaires catégorielles, l’intégration de la morphologie et de la syntaxe, le calcul de représentations sémantiques à partir d’analyses syntaxiques (catégorielles, minimalistes,...), la résolution d’anaphores, le passage de la structure prédicative de la phrase à la structure logique du discours.
Les algorithmes correspondants, d’analyse, de génération ou d’acquisition seront programmés dans des langages de même nature logique (OCaML),
et la démonstration assistée par ordinateur (Coq) sera utilisée pour établir les propriétés des systèmes formels utilisés.

Ces techniques sont mises en oeuvre à travers deux applications :
 réalisation d’un site navigable de la littérature en sanskrit
 génération d’énoncés en langue des signes française