Institut de Mathématiques de Luminy

RAPPORT D'ACTIVITÉ

LOGIQUE DE LA PROGRAMMATION

1. INTRODUCTION
2. THEMES DE RECHERCHE PRINCIPAUX
  2.1.   Focalisation, logique polarisée ludique et logique locative
2.2.   Sémantique dénotationnelle
2.3.   Lambda-calcul et réseaux différentiels
2.4.   Réseaux de preuves et d'interaction
2.5.   Systèmes à complexité bornée
2.6.   Logique et quantique
2.7.   Logique et philosophie
2.8.   Réécriture en dimension supérieure
2.9.   Combinatoire des graphes et des relations
2.10. Algorithmique pour la sûreté du fonctionnement
3. ACTIVITES EXTERNES

1. INTRODUCTION

Initialement centré sur le paradigme de Curry-Howard (programmes vus comme preuves logiques), ce thème a tendu ces dernières années à s'élargir, couvrant désormais plus largement les liens que les mathématiques entretiennent avec la théorie du calcul et de la programmation.

Le paradigme de Curry-Howard reste central. Il s'agit à l'origine de la constatation d'un isomorphisme entre les preuves intuitionnistes et le lambda-calcul typé (formules/types, preuves/termes, élimination des coupures/bêta-réduction). Il a été largement étendu : à la logique classique en particulier (les principes classiques, comme la loi de Pierce, correspondant à des primitives de programmation "non locales" comme les exceptions et le continuations, bien connus des informaticiens) et bien sûr à la logique linéaire, qui est dès le départ un raffinement de la logique intuitionniste Curry-Howard. La logique linéaire a permis notamment la mise au point de nouvelles représentations plus géométriques des preuves/programmes : les réseaux de preuves et les réseaux d'interaction. Elle a également permis une nouvelle analyse du calcul, associant aux preuves des opérateurs sur des espaces de Hilbert : la géométrie de l'interaction. Par ce biais, des liens longtemps pressentis entre logique et mécanique quantique semblent devoir prendre corps. Enfin, le contrôle des règles structurelles que fournit la logique linéaire permet de construire des systèmes logiques dans lesquels la complexité de l'élimination des coupures est bornée (élémentairement ou polynomialement) ce qui à terme pourrait mener à des langages de programmation à complexité bornée. La correspondance de Curry-Howard comporte par ailleurs un volet sémantique dénotationnelle où les formules/types sont interprétés par des espaces abstraits et les preuves/programmes par des morphismes entre ces espaces.

Dans le même esprit, une nouvelle direction de recherche a pris de l'importance ces dernières années dans notre thème : celle d'une approche basée plus directement sur une modélisation géométrique du calcul, et plus spécifiquement, de la réécriture. Dans ce cadre, les termes sont vus (par exemple) comme des objets de dimension 2 (typiquement, des 2-morphismes dans une N-catégorie, ou des 2-cellules dans un complexe), les réécritures comme des objets de dimension 3, les "standardisations" (transformations de chemins de réécritures) comme des objets de dimension 4, etc. Ce point de vue donne lieu à des développements de nature homotopique, dans l'esprit de l'étude du problème du mot en dimension supérieure entreprise par Albert Burroni, ou homologique, dans la suite des travaux de Craig Squier.

Enfin, notre thème comporte également une direction combinatoire qui s'occupe de théorie des graphes et de théorie des relations, tout particulièrement du point de vue des questions de décomposition et de reconstruction, ainsi qu'une composante qui s'occupe d'algorithmique pour la sûreté de fonctionnement.

2. THÈMES DE RECHERCHE PRINCIPAUX

2.1. Focalisation, logique polarisée ludique et logique locative

La propriété de focalisation (Andreoli) est à l'origine de la polarisation de la logique linéaire, qui se comprend mieux du point de vue "recherche de preuve". Si on a un séquent à prouver, le travail consiste à choisir une formule dans ce séquent, qui aura donc un connecteur logique principal, et à choisir une règle d'introduction (nous sommes en calcul des séquents, donc toutes les règles logiques sont des règles d'introduction) pour ce connecteur. On applique ensuite cette règle, vue comme une façon de décomposer le séquent, puis on recommence sur les prémisses ainsi construites, le but étant de fabriquer de cette façon un arbre de preuve dont le séquent à prouver sera à la racine. La remarque fondamentale est que, de ce point de vue, les connecteurs se divisent en deux catégories :

- Les connecteurs négatifs, qui sont réversibles: cela signifie que les règles correspondantes peuvent être effectuées n'importe quand (en particulier, immédiatement) ; l'ensemble des prémisses est en quelque sorte équivalent à la conclusion.

- Ce n'est pas le cas des connecteurs positifs : en sélectionnant un connecteur positif et une règle pour ce connecteur, on fait un choix qui engage toute la poursuite du processus. Mais les connecteurs positifs ont la propriété de focalisation, en quelque sorte duale de la réversibilité (d'ailleurs, les connecteurs positifs et négatifs sont duaux de De Morgan vis-à-vis de la négation linéaire) : une fois choisie la formule positive, on peut (sans risque de manquer davantage de preuves que celles qu'on a pu manquer par le choix initial) continuer à la décomposer, tant qu'on continue à ne rencontrer que des connecteurs positifs ; on dit qu'on peut focaliser sur cette formule.

Paul Ruet et Roberto Maieli (université Rome 3) ont montré que cette structure fondamentale de la logique (qui est par exemple à l'origine de la ludique) se retrouve également dans le cadre de la logique non commutative étudiée par Paul Ruet dans ses précédents travaux. Plus précisément, ils ont introduit un calcul des séquents explicitement polarisé pour la logique non commutative et montré qu'il est équivalent au calcul des séquents ordinaires, à base de variétés d'ordre.

Sous la direction de Paul Ruet, Anne Crumière travaille sur la complexité de la prouvabilité de certaines logiques, notamment en ce moment sur la logique linéaire multiplicative non-associative. Elle commence à regarder la logique Q-permutative. L'objectif est d'établir des critères pour classer les variétés d'ordre selon leur complexité de prouvabilité.

Jean-Yves Girard a développé ces dernières années la ludique, une nouvelle approche de la logique basée sur les effets de polarisation et de focalisation. Dans ce cadre, l'objet fondamental de la logique n'est plus la preuve, mais le dessein, sorte de preuve non typée, normale et polarisée, dans laquelle les formules sont remplacées par des loci qui sont des pointeurs correspondant à la notion d'occurrence de sous-formule en logique (on dit que le système est locatif, au sens où cette notion d'occurrence est prise au sérieux). Les desseins sont sujet à un mécanisme d'élimination des coupures très général, permettant de définir le concept fondamental de comportement qui correspond à la notion habituelle de formule. Ces travaux ont été prolongés par Marie-Renée Fleury et Myriam Quatrini : elles ont proposé une interprétation des quantificateurs du premier ordre en ludique qui permet d'étendre aux formules d'un calcul des prédicats linéaire le résultat de complétude établi par Jean-Yves Girard pour un calcul des séquents linéaire du second ordre avec des connecteurs multiplicatifs et additifs. En collaboration avec Claudia Faggian (université de Padoue), elles ont par ailleurs développé une analyse du concept d'uniformité en ludique.

Thomas Ehrhard a obtenu un théorème de complétude pour la logique linéaire indexée, système locatif lui aussi, qu'il avait développé précédemment avec Antonio Bucciarelli (PPS). Il s'agit d'une complétude vis-à-vis d'une notion d'espaces de phase indexés symétriques mise au point en même temps que cette logique, et permettant de définir de nouveaux modèles dénotationnels de la logique linéaire "au dessus" du modèle relationnel standard.

Jean-Marc Andreoli s'est intéressé à la construction de preuves de calcul des séquents par propagation de contraintes, la construction se faisant par expansions successives des noeuds ouverts d'un arbre de preuve dont les noeuds sont étiquetés non pas par des séquents explicites (comme c'est le cas classiquement) mais par des variables (séquents implicites) liés entres elles par des contraintes. La construction se transforme donc en un problème de propagation de contraintes.

2.2. Sémantique dénotationnelle

Pierre Boudes a poursuivi le travail commencé dans sa thèse (soutenue fin 2002) sur le lien entre les modèles de jeux et la sémantique relationnelle de la logique linéaire, et en particulier le modèle des hypercohérences introduit par Thomas Ehrhard en1993. Ce faisant, il a naturellement été amené à se limiter à des fragments polarisés (au sens du paragraphe ci-dessus) de la logique linéaire, car c'est seulement pour de tels fragments que l'on dispose de modèles de jeux qui se comportent bien, comme la thèse d'Olivier Laurent (actuellement membre de PPS et ex-thésard de LDP) l'a montré. Dans ce cadre polarisé, il a développé une théorie de l'"écrasement" (oubli de la temporalité) des stratégies sur les cliques, et conjecturé l'injectivité de cet écrasement. Il ne s'agit pas simplement ici de répondre à une question technique, mais de comprendre si la temporalité explicite présente dans les jeux est vraiment nécessaire.

Thomas Ehrhard a continué d'explorer le modèle dénotationnel des espaces de finitude, montrant notamment comment associer un espace vectoriel topologique à un espace de finitude. Les topologies correspondantes sont linéaires au sens où 0 admet une base de voisinages composée uniquement de sous-espaces ; le corps est muni de la topologie discrète. De telles structures, peu usuelles, avaient déjà été considérées par Lefschetz en1942 et s'avèrent parfaitement adaptées ici. Thomas Ehrhard a obtenu des résultats de clôture monoïdale (les morphismes étant les fonctions linéaires continues) et cartésienne (les morphismes étant des sortes de séries entières).

Actuellement en troisième année de thèse sous la direction de Thomas Ehrhard et de Thierry Coquand (université Chalmers à Göteborg), Pierre Hyvernat a poursuivi son étude des "systèmes d'interaction". Cette structure mathématique permet de modéliser les spécifications de programmes informatiques et entretient des rapport avec diverses branches de la logique mathématique. Les deux thèmes principalement étudiés sont :

- la modélisation des "topologies formelles", une version prédicative des locales ou "frames" qui forment l'objet d'étude de la "topologie sans points" ;

- la pertinence de cette structure en tant que modèle dénotationnel de la logique linéaire, et au fait que le modèle obtenu modélise également la lambda-calcul différentiel.

2.3. Lambda-calcul et réseaux différentiels

Thomas Ehrhard et Laurent Regnier ont introduit en logique des constructions inspirées du calcul différentiel, comme le suggère le modèle dénotationnel des espaces de Köthe et des espaces de finitude étudiés par Ehrhard. En particulier, ils ont défini un lambda-calcul différentiel dont ils ont établi les propriétés de base : confluence, normalisation forte dans le cas typé. Ils ont analysé dans ce cadre le développement de Taylor et l'ont relié à la réduction linéaire de tête (la procédure d'évaluation des lambda-termes implémentée par la machine de Krivine). Ce travail établit un lien étroit entre dérivation, au sens de l'analyse, et substitution linéaire, au sens du lambda-calcul et de la logique linéaire.

Ils ont ensuite généralisé le résultat qu'ils avaient obtenus à propos du développement de Taylor en 0 des lambda-termes purs, en considérant la situation où toutes les applications d'un lambda-terme sont développées de Taylor. On obtient alors alors une combinaison linéaire infinie (à coefficients rationnels) de termes ne comportant que des "applications différentielles" itérées, et des applications à 0, ce qui s'exprime dans un calcul plus simple que le lambda-calcul différentiel, très proche du lambda-calcul avec ressources introduit par Gérard Boudol (INRIA-Sophia), avec des motivations complètement différentes.

Ils ont également étudié l'extension de la logique linéaire qui correspond au lambda-calcul différentiel, constatant que cette extension consiste à ajouter à la logique linéaire des règles qui sont les duales exactes des règles, standard, d'affaiblissement, de contraction et de déréliction. Ces nouvelles règles (co-affaiblissement, qui correspond à l'application d'une série entière à 0, co-contraction, qui correspond à l'application à une somme, et co-déréliction, qui correspond à la dérivation en 0) interagissent de façon complètement symétrique avec leurs analogues standard, ce qu'illustre parfaitement la présentation de ce nouveau système dans le cadre des réseaux d'interaction (réseaux d'interaction différentiels).

Sous leur direction conjointe, Lionel Vaux a commencé un travail de thèse visant à généraliser à la logique classique (et plus précisément, au-calcul de Parigot) l'extension différentielle du lambda-calcul. L'intérêt de ce travail réside notamment dans le fait que les constructions différentielles interagissent avec les constructions structurelles, comme on l'a vu, et que ces dernières se voient généralisées dans la logique classique.

2.4. Réseaux de preuves et d'interaction

Dans son travail sur la construction incrémentale de preuves, Jean-Marc Andreoli s'est également intéressé au cas des réseaux de démonstration de la logique linéaire. Dans ce cadre, il s'agit de produire un critère de correction incrémental, puisqu'il faut être capable, à chaque étape de la construction incrémentale (ajout d'un nœud positif ou négatif), de déterminer si l'on construit bien un "réseau partiel". Cette construction fournit une modélisation logique de l'accès concurrent à une base de donnée.

Au cours de son stage de DEA et de sa première année de doctorat, sous la direction de Laurent Regnier, Damiano Mazza s'est occupé d'étudier le lien entre calculs de processus pour la mobilité et logique (en particulier logique linéaire et ludique), avec le but de comprendre si et jusqu'où il est possible d'étendre la correspondance de Curry-Howard au domaine de la concurrence. Après avoir étudié le rapport entre fonctions (au sens de la programmation fonctionnelle) et processus, il a examiné la possibilité de ramener le pi-calcul à un calcul de réécriture de graphes. Pour cela, il a défini une extension non-déterministe des réseaux d'interaction de Yves Lafont (déjà considérée par Vladimir Alexiev dans sa thèse de doctorat) et démontré qu'il existe une traduction simple et fidèle du pi-calcul sans sommes dans ces systèmes.

2.5. Systèmes à complexité bornée

Peu après la découverte de la logique linéaire, Jean-Yves Girard, Philip Scott et André Scedrov ont proposé un premier système dont l'élimination des coupures (réduction) est en temps polynomial, mais ce système BLL comportait des polynômes explicites. Jean-Yves Girard a ensuite introduit les systèmes ELL (complexité élémentaire) et LLL (complexité polynomiale), en affaiblissant les règles logiques associées aux exponentielles. Vincent Danos et Jean-Baptiste Joinet (PPS) ont étudié les réseaux de preuves associés à LLL et ELL. Yves Lafont a ensuite découvert un troisième système à complexité polynomial, SLL.

Dans le cadre de son travail de thèse actuellement en cours, sous la direction conjointe de Thomas Ehrhard et de Patrick Baillot (LIPN), Daniel de Carvalho s'est intéressé au problème de typer les termes d'un lambda-calcul mis au point par Kazushige Terui, et dont la réduction est en temps polynomial. Cette propriété de complexité est en effet indépendante du système de type naturel associé à ce lambda-calcul (la logique affine légère), et le calcul normalise en temps polynomial y compris pour les termes non typés. Toutefois, dans le cas non typé, la réduction peut mener à des termes erronés (des sortes de "deadlocks"). Daniel de Carvalho a réussi à caractériser précisément tous les termes pour lesquels ce n'est pas le cas, au moyen d'un système de types avec intersections, beaucoup plus faible bien sûr que la logique linéaire légère (et donc admettant beaucoup plus de termes, c'est-à-dire, beaucoup plus d'algorithmes polynomiaux).

Il étudie à présent les modèles dénotationnels de la logique linéaire légère, en essayant de s'affranchir de la structure stratifiée que Patrick Baillot avait utilisée dans les siens, structure qui reflète le caractère stratifié des preuves (en termes de boîtes). Daniel de Carvalho cherche dans une autre direction, visant à interpréter directement, en termes de complexité algorithmique, les multi-ensembles qui interviennent dans l'interprétation relationnelle des exponentielles de la logique linéaire.

Signalons que cette thèse est financée par une allocation obtenue dans le cadre de l'ACI GEOCAL.

Sous la direction de Regnier, Damiano Mazza a également étudié ces "logiques allégées", ELL et LLL. Il a étendu le travail de Danos-Joinet sur les réseaux pour ELL, et obtenu ainsi une notion élégante de réseau pour LLL. Rappelons que les réseaux de preuves fournissent un outil précieux d'analyse des programmes en lambda-calcul, aussi cette définition de réseaux polynomiaux devrait s'avérer importante dans l'étude du temps polynomial en logique.

2.6. Logique et quantique

Jean-Yves Girard a travaillé sur l'interprétation de la logique dans les algèbres d'opérateurs. Il a développé la notion d'espaces cohérents quantiques, dans lesquels les cliques des espaces cohérents ordinaires sont remplacés par certains opérateurs hermitiens sur un espace de Hilbert. Il a poussé plus loin son analyse de l'élimination des coupures en terme de géométrie de l'interaction, dans laquelle l'élimination des coupures s'exprime comme la résolution d'une équation du feedback qu'il a montré comment résoudre de façon très générale, dans un cadre d'algèbres d'opérateurs. Jean-Yves Girard a par ailleurs donné un cours de théorie de la démonstration de octobre à décembre 2004, à Rome, dans le cadre de l'université franco-italienne. Ce cours a donné lieu à un livre actuellement à l'état de manuscrit (460 pp.).

2.7. Logique et philosophie

Sous la direction conjointe de Jean-Yves Girard et de Pierre Livet (université Aix-Marseille 1 et CEPERC), Samuel Tronçon a poursuivi son travail de thèse (Dynamique des démonstrations) qui porte sur la philosophie de la logique et vise à présenter une analyse contemporaine de la théorie de la démonstration et de ses rapports avec la cognition, l'informatique et la signification. Pendant ces deux années, deuxième phase de sa thèse, ses recherches ont porté avec de plus en plus d'insistance sur la synchronisation des recherches logiques et des ambitions contemporaines visant à développer de nouvelles théories de la signification et de la cognition. Il a longuement étudié la façon dont on pourrait étendre la correspondance de Curry-Howard à ces domaines, et notamment les intuitions philosophiques (holisme, jeux de langage, signification par l'usage...) qui pourraient être confirmées par certains progrès techniques réalisés en théorie de la démonstration (Lambda-Calcul, Logique Linéaire, Ludique). Il a largement contribué à l'animation du groupe "Logique et Interaction : vers une Géométrie de la Cognition" (LIGC) ; voir :

http://www-philo.univ-paris1.fr/Joinet/ligc.html

Dans le cadre de ce groupe LIGC, Jean-Yves Girard a rédigé un tract qui doit être publié dans un volume collectif aux Presses de la Sorbonne.

En 2003, Myriam Quatrini a participé à un groupe de travail interne à LDP et animé par Samuel Tronçon. Myriam Quatrini envisage de réorienter son activité de recherche autour de ces sujets. En particulier, elle s'intéresse aux applications possibles des idées récentes de la théorie de la démonstration pour le développement de nouveaux outils d'analyse textuelle adaptés aux préoccupations des SHS et à la transposition de ces idées pour la formalisation des méthodes en SHS. Une première étape dans cette direction est son engagement depuis le début de l'année 2004, dans un projet pluridisciplinaire articulant sciences humaines et sociales (histoire et philosophie du langage), mathématiques (statistiques et logique) et informatique (traitement automatique du langage). L'équipe constituée autour de ce projet se propose d'étudier les processus à l'œuvre dans l'émergence et l'évolution de concepts (de nature, d'aménagement du territoire et d'environnement) et la constitution de discours d'une communauté (les ingénieurs des ponts et chaussées du 19ème siècle).

2.8. Réécriture en dimension supérieure

Yves Lafont a commencé à travailler avec François Métayer (PPS) sur la "théorie homotopique du calcul". La notion clef de cette théorie est celle de "résolution" (non commutative) de Métayer, qui s'exprime elle-même en termes de "polygraphes" de Burroni ou de "computades" de Street. Cette notion devrait permettre d'unifier et de généraliser des approches qui sont visiblement apparentées comme les théorèmes de cohérence en théorie des catégories (Mac Lane et autres), les invariants homologiques et homotopiques de la réécriture (Squier et autres), ou l'homologie des groupes Gaussiens (Patrick Dehornoy et Yves Lafont). Dans cet esprit, ils ont dressé une liste d'une quinzaine de conjectures ou de directions de recherche (Programme de Minneapolis).

Yves Guiraud a étudié le système de réécriture de diagrammes proposé par Yves Lafont dans son article sur la théorie algébrique des circuits booléens, en vue de voir si les techniques de preuve de confluence qu'il avait développées dans sa thèse pouvaient s'appliquer. Il a montré que ce système était convergent, ce qui montre bien l'intérêt de sa méthode : c'est sans doute le premier exemple convainquant d'un tel système qui n'est pas issu de la réécriture de terme.

Par ailleurs, il a résumé une partie de son travail de thèse dans un document intitulé "Termination orders for 3-dimensional rewriting", actuellement soumis pour publication. De plus, il a commencé à compléter un secteur laissé inachevé dans sa thèse : l'étude de la confluence des 3-polygraphes ou systèmes de réécriture de dimension 3. Enfin, il a initié un travail visant à interpréter les démonstrations et leurs transformations comme des objets respectivement tridimensionnels et quadridimensionnels, spécifiés par un 4-polygraphe.

Yves Guiraud a été recruté sur un demi-poste d'ATER à l'IML pour travailler dans cette nouvelle direction de recherche. Il anime un groupe de travail sur la réécriture en dimension supérieure au sein de LDP.

2.9. Combinatoire des graphes et des relations

Pierre Ille a principalement poursuivi sa recherche sur la décomposabilité, pour la somme lexicographique, des structures combinatoires. En généralisant l'arbre de décomposition au cas infini, il a résolu la conjecture de Sabidussi (1960) sur les graphes idempotents pour le produit lexicographique. Concernant les structures infinies et indécomposables, il a caractérisé les graphes critiques et, pour les fortement critiques, a précisé son résultat à l'aide de l'arbre de création sous-jacent. Dans le cas fini, il a abordé le problème de recouvrement par des sous-structures indécomposables et celui de la reconnaissance de l'indécomposabilité à partir de différentes hypothèses locales. D'autres travaux ont été menés en théorie des ordres : dénombrement des réalisateurs, reconstruction et monomorphie. Enfin, avec Paul Ruet, il a résolu un problème de complexité algorithmique sur les variétés d'ordre, structures combinatoires qui jouent un rôle fondamental en logique non commutative.

2.10. Algorithmique pour la sûreté du fonctionnement

Antoine Rauzy travaille sur la sûreté de fonctionnement de système, c'est-à-dire l'ensemble des méthodes qui permettent d'évaluer le risque et les conséquences du risque dans des installations industrielles sensibles : centrales nucléaires, industries chimiques et pétrolières, avionique, transports... Pour évaluer le risque, les ingénieurs font des modèles et emploient donc des formalismes de description. Ces derniers sont principalement des formalismes Booléens ou des formalismes états/transitions (automates d'états finis, réseaux de Petri ...) Une fois l'installation décrite par un modèle, il faut se servir de ce modèle pour évaluer les quantités (en général probabilistes) qui donnent une mesure du risque (probabilité ou fréquence des accidents/incidents) et de ses conséquences (gravité, impact sur l'environnement, impact économique ...) Ce processus soulève deux problèmes, liés entre eux:

- Comment modéliser de façon à avoir une bonne image du système étudié. Cela implique d'avoir des formalismes de modélisation adé\-quats (ce n'est pas du tout trivial car il faut que les modèles "vivent" avec les systèmes).

- Comment traiter les modèles sachant que la plupart des problèmes à résoudre sont NP-difficiles ou #P-difficiles.

Son travail depuis 10 ans (et pour les 10 ans à venir) consiste à avancer dans les deux directions : d'une part par la mise au point de formalismes de description et de méthodologies de modélisation, d'autre part par la mise au point d'un corpus d'algorithmes et d'heuristiques permettant de repousser aussi loin que possible les limites de l'explosion combinatoire.

3. ACTIVITÉS EXTERNES

Depuis septembre 2003, notre thématique participe à un projet d'ACI Nouvelles Interfaces de Mathématiques intitulé "Géométrie du Calcul" (GEOCAL), et dont Thomas Ehrhard est le responsable. Ce projet, qui doit durer 3 ans, regroupe 10 équipes travaillant sur des sujets liés aux directions de recherche ci-dessus, et a donc été l'occasion d'accroître l'interaction de notre équipe avec nos collègues, au travers notamment de l'organisation de rencontres scientifiques (6 jusqu'à présent) et de nombreuses missions entre les sites. On en trouvera une description plus précise en :

http://iml.univ-mrs.fr/ehrhard/geocal/

D'autre part, Thomas Ehrhard et Yves Lafont ont participé à l'Action Spécifique "Topologie Algébrique pour l'étude des structures de calcul et notamment de la concurrence" (responsable : Eric Goubault, PPS) qui s'est terminée en 2004 et a trouvé un prolongement naturel dans GEOCAL.

En coopération avec Michele Abrusci de l'université de Rome 3, l'équipe a mis en place un réseau de formation doctorale, intitulé "Logique mathématique et informatique théorique", entre l'Université de la Méditerranée et l'Université de Rome 3, qui a reçu le financement de l'Université Franco-Italienne pour l'année 2002-2003 et l'année 2003-2004. Ce réseau, coordonné par Paul Ruet, a permis de favoriser la mobilité des doctorants et des chercheurs entre Marseille et Rome, et a notamment participé à l'organisation du cours de théorie de la démonstration de Jean-Yves Girard à l'automne 2004 à l'université Rome 3, en octobre, novembre et décembre 2004.

 

Page d'accueil
Sommaire