Nouvelles chaires

Droit, culture et société de la Rome antique

Le Collège de France crée une chaire dédiée au droit de la Rome antique en la confiant à l’un des spécialistes les plus reconnus au plan international dans cette discipline, Dario MANTOVANI. Juriste historien, passé par les universités de Trente, Parme et Pavie, il a consacré sa carrière à l’étude du droit romain avec le souci constant de le replacer dans les milieux de sa production et de son fonctionnement :

« Ma méthode – je devrais dire mon souhait – consiste à comprendre le droit romain du point de vue de la société qui l’a produit, c’est-à-dire tel qu’il a été pensé, pratiqué et traduit dans des textes. »

Chaire nouvelle, qui répond à un intérêt renouvelé pour cette discipline, en Europe comme en Amérique, mais qui a déjà une histoire imposante derrière elle car c’est autour des textes de droit romain – le Corpus Iuris Civilis de Justinien – que sont nées les universités. Elles ont répandu en Europe une culture qui a constitué un des liens les plus forts dans la construction d’une vision commune du droit. Devenus ensuite avocats, juges ou fonctionnaires, les étudiants portèrent avec eux et réélaborèrent des idées qui ont été fondamentales pour la construction européenne de l’idée de justice et d’État de droit : C’est ainsi que le droit d’une cité antique est devenu une forme de pensée commune à une grande partie de l’Occident jusqu’aux Temps modernes.

« Le Corpus Iuris Civilis de Justinien a été en quelque sorte le roman d’apprentissage de l’Europe. Si l’on considère le succès considérable que le droit romain a eu à partir du XIe siècle, réactiver la compréhension de ce riche patrimoine interprétatif signifie se réapproprier une clé d’intelligibilité de la tradition juridique européenne ».

La première série de cours de Dario MANTOVANI (année 2018-2019) sera consacrée aux usages juridiques du passé (dans la pensée des juristes romains).

Les séminaires seront l’occasion de présenter des fragments inédits d’œuvres des juristes romains identifiés dans les papyrus et publiés par l’équipe REDHIS (projet « Ré-explorer la « structure cachée ». Une nouvelle appréciation des textes et des formes de la pensée juridique dans l’antiquité tardive » soutenu par le conseil européen de la recherche / ERC et dirigé par le Pr Dario MANTOVANI) : une présentation qui veut susciter le débat sur les nouvelles perspectives que ces documents apportent sur une diffusion jusqu’ici insoupçonnée des œuvres des juristes dans l’Antiquité tardive.

Leçon inaugurale : jeudi 17 janvier 2019 à 18h00

Sciences du logiciel

Les travaux de recherche de Xavier LEROY portent d’une part sur les nouveaux langages et outils de programmation, et d’autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité.  Il est l’architecte et l’un des principaux développeurs du langage de programmation fonctionnelle OCaml ainsi que du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.

Langages fonctionnels, systèmes de types et mise en pratique : les langages Caml Light et OCaml

Xavier LEROY a été formé aux mathématiques et à l’informatique à l’École normale supérieure, puis à l’INRIA où il a effectué sa thèse. Programmeur prodige, il s’est illustré par une série de travaux de premier plan sur les systèmes de types et les systèmes de modules pour les langages fonctionnels, qui ont abouti au développement de Caml Light, devenu aujourd’hui OCaml, l’un des deux langages fonctionnels typés les plus utilisés au monde, dans des domaines aussi divers que l’aéronautique, la finance ou encore le Web. Ce langage est le support de développement d’outils logiciels très variés comme l’assistant de preuve Coq, les analyseurs statiques Astrée et Frama-C, le compilateur SCADE 6 d’Estérel Technologies et la blockchain Tezos. OCaml a été utilisé dans de nombreux projets emblématiques comme la version web de Facebook Messenger, le logiciel MediaWiki ou encore l’infrastructure de virtualisation Docker.

Preuve de programme, preuve de compilateurs et mise en pratique : le compilateur CompCert 

Xavier LEROY est également à l’origine de CompCert, qui est un compilateur C certifié, écrit et vérifié grâce à l’assistant de preuve Coq. Il s’agit d'une première mondiale à plusieurs titres : il autorise une vérification formelle d’une taille et d’une complexité sans précédent, et surtout, il offre la possibilité de disposer d’un compilateur certifié, étape clé dans la certification et la vérification automatique des chaînes logicielles, et donc vers la programmation « zéro défaut ». Ce fait d’arme a eu un impact considérable sur la nature même des grands programmes de recherche sur les logiciels.

 
Nommé professeur au Collège de France, Xavier LEROY occupera la chaire Sciences du logiciel où il dispensera dès l’année académique 2018-2019 une série de cours intitulée
Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui.

Leçon inaugurale jeudi 15 novembre 2018 à 18h00