ANR-PRELUDE

Structures Formelles du Langage

2007-04-25T20:31:32Z

Axes de recherche :

– Développement d'une théorie minimaliste de la syntaxe et de la morphologie,

– Langues et grammaire,

– Acquisition des langues,

– Poétique et métrique comparées.

– Formalisation de la modalité visuo-gestuelle

– Les travaux de l'unité portent sur la comparaison et la typologie des langues naturelles (y compris les langues signées), les formalismes grammaticaux, l'organisation interne des divers composants (syntaxe, morphologie, phonologie) et les relations d'interface entre eux, la poétique et la métrique,

– Le traitement des langues naturelles par le sujet parlant (acquisition des langues, langues des signes, construction du discours).

SIGNES

2007-04-25T20:21:22Z

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

Logique de la Programmation

2007-04-25T19:52:05Z

L'équipe Logique de la Programmation est une équipe de recherche de l'Institut de Mathématiques de Luminy, UMR 6206 du CNRS. Fondée par Jean-Yves Girard en 1992, l'équipe LDP fait porter sa recherche sur la logique mathématique, la théorie de la démonstration et la théorie du calcul, ainsi que sur les interactions entre ces théories et d'autres disciplines, notamment les mathématiques, l'informatique, la linguistique, la philosophie et la biologie.

L'équipe a de nombreuses collaborations avec des laboratoires en France (Marseille, Paris, Montpellier, Sophia-Antipolis, Grenoble, Chambéry, Nancy) et à l'étranger (Italie, Royaume-Uni, Allemagne, Canada, Etats-Unis, Japon). Au niveau local elle participe aux activités de la FRUMAM, et organise un groupe de travail avec des chercheurs du LIF.

Elle coordonne l'ACI Géométrie du Calcul, et participe à l'AS Topologie Algébrique pour l'étude des structures de calcul, et notamment de la concurrence, au Master Recherche de Mathématiques Discrètes et Fondements de l'Informatique et au Master Professionnel de Mathématiques et Informatique des Nouvelles Technologies.

Sur le plan scientifique l'équipe s'est récemment ouverte à de nouveaux champs d'application : théorie homotopique du calcul, combinatoire des relations, vérification automatique, logique et philosophie, systèmes discrets et biologie. Le paradigme initial est la correspondance de Curry-Howard, qui relie preuves et formules logiques aux concepts informatiques de programmes (termes du lambda-calcul) et types. Ce paradigme est à l'origine d'un grand nombre de développements (notamment la logique linéaire de Girard), sujets de recherche pour plusieurs membres de LDP.

CALLIGRAMME

2007-04-25T20:16:32Z

Le thème de recherche de CALLIGRAMME est l'utilisation de la logique linéaire et, en particulier de la théorie des réseaux de démonstration dans la modélisation de la circulation de l'information. Deux cas spécifiques de circulation de l'information sont envisagés : dans les calculs de processus, l'information communiquée entre agents ; dans le cas de l'analyse grammaticale, l'information syntaxique échangée entre les constituants d'un même syntagme.

Axes thématiques
• Réseaux de démonstration et d'interaction
• Logique linéaire et parallélisme
• Logique linéaire et grammaires formelles
• Calculs lambda typés et sémantiques

Un des objectifs applicatifs de ces quatre actions de recherche est la mise au point d'un modèle grammatical basé sur la logique linéaire permettant d'intégrer diverses théories linguistiques.

Relations scientifiques et industrielles
• Coopération avec le laboratoire de recherche Xerox à Grenoble
• Collaboration avec l'Institut de Mathématiques de Luminy
• Nombreux échanges avec des centres universitaires : Imperial College, Universités d'Utrecht, de Rome III, d'Indiana, de Catalogne, de la Sarre, de Pennsylvanie