Podcasts about l'inria

durée : 00:05:48 - franceinfo junior - L'exposition internationale de robots, iRex, se tient à Tokyo jusqu'au 2 décembre. Jean-Baptiste Mouret, ingénieur et chercheur en robotique et intelligence artificielle à l'INRIA, répond aux questions des enfants de franceinfo junior.

La startup française Dynalips, née dans les labos de l'INRIA et de LORIA, a mis au point une technologie de synchronisation labiale pour rendre encore plus réaliste l'animation de personnages en réalité virtuelle. Destinée à l'industrie du cinéma et du jeu vidéo, cette technique à base d'IA se veut éthique et inutilisable pour la création de fake news. Louis Abel, doctorant de l'Université de Lorraine et co-fondateur de Dynalips, expilque les enjeux qui se cachent derrière cette technologie en apparence anodine. 

durée : 00:39:49 - Le Temps du débat - par : Emmanuel Laurentin - Le 10 mars, le ministre français du numérique a reçu des responsables de Tiktok. L'application chinoise préoccupe : addiction de jeunes publics, protection des données et sécurité. Pour tenter de l'encadrer, les pouvoirs publics font fleurir les restrictions en Europe et en Amérique du Nord. - invités : Stéphane Taillat maître de conférences en relations internationales à l'Institut français de géopolitique de Paris 8; Serge Abiteboul Informaticien, membre du Collège de l'Arcep, chercheur à l'ENS Paris et directeur de recherche à l'Inria; Laurence Allard maîtresse de conférence en sciences de la communication, enseigne à l'Université de Lille en études culturelles, chercheure à l'IRCAV, (Institut de Recherche sur le Cinéma et l'Audiovisuel) / Paris 3 Sorbonne Nouvelle.

durée : 00:38:38 - Le Temps du débat - par : Quentin Lafay - Depuis le 20 mars, l'Assemblée discute de l'autorisation temporaire de dispositifs de vidéosurveillance algorithmique pour les Jeux Olympiques de 2024, ce que la Cnil qualifie de « tournant ». Déjà à l'expérimentation, cette technologie peut-elle se porter garante de la sécurité comme des libertés ? - invités : François Brémond directeur de recherche à l'INRIA à Sophia Antipolis; Katia Roux chargée de plaidoyer Libertés à Amnesty International France

durée : 00:26:26 - L'invité de 8h20 : le grand entretien - par : Jérôme CADET - Isabelle Ryl, chercheuse à l'Inria, Cédric Villani, l'auteur du rapport "Donner un sens à l'intelligence artificielle" remis en mars 2018, et Cécile Badoual, cheffe de service en anatomo-pathologie à l'hôpital Pompidou, échangent à propos de l'intelligence artificielle.

Room juridique d'Ingrid, spécial rapport interministériel sur “la mission exploration sur le Metavers” avec Me Adrien Basdevant avocat au barreau de Paris, spécialisé dans l'innovation numérique et ses impacts sur la société, qui a participé à sa rédaction avec Camille François, chercheuse spécialisée dans les opérations informationnelles sur les réseaux sociaux à l'université de Columbia et Rémi Ronfard, chercheur à l'Inria spécialisé dans l'animation 3D et la cinématographie virtuelle.Entretien portant sur :- la définition proposée après une exploration interdisciplinaire.- vers un Ministère du Metavers suite aux 10 recommandation.- les adaptations possibles du droit numérique Web2- le nouvel enjeu spécifique : EDI, identité autonome décentralisée.Pour aller plus loin:* Le rapport interministériel: “Mission exploratoire sur le Métaverse”* Compte LinkedIn de Me Adrien Basdevant* Compte LinkedIn de Me Ingrid-Méry Haziot This is a public episode. If you would like to discuss this with other subscribers or get access to bonus episodes, visit www.nftmorning.com

Stéphane Grumbach directeur de recherche à l'INRIA membre du projet GEODE qui traite de la géopolitique de la datasphère et enseignement à Science Po et auteur de "L'empire des algorithmes". Les implications des technologies de l'information se voient au niveau individuel, il suffit de prendre le métro pour voir tout le monde absorbé par son smartphone, mais également au niveau international : les rapports entre les états ont changé. Il y a également une opposition typique du numérique qui se joue entre d'une part la concentration des informations et d'autre part la distribution (au sens informatique distribuée) des informations. Entre Charybde et Scylla, nous discutons aujourd'hui de cette révolution virtuelle.

La première actualité de cet épisode, c'est tout simplement l'information selon laquelle Salto, plateforme de streaming vidéo de TF1, M6 et France Télévision, serait à vendre. La seconde actualité concerne le partenariat entre l'Inria et Hive, pour créer un géant français du cloud. Sans oublier : Amazon Alexa serait un échec commercial à 10 milliards de dollars en 2022, et Ubisoft est réellement de retour sur Steam.Les autres épisodes sont aussi disponibles sur Siècle Digital. Hébergé par Acast. Visitez acast.com/privacy pour plus d'informations.

Alastair Abbott est chercheur à l'Inria basé à Grenoble. Il est spécialisé en théorie de l'information quantique, à la croisée des chemins entre la physique quantique et les sciences de l'information. Cela couvre un grand nombre de domaines : les structures de contrôle quantique, la correction d'erreurs, les communications quantiques, les fondations de la physique quantique, et les théories de l'algorithmie quantique. Tout un programme ! Il avait été auparavant post-doc à l'Université de Genève dans le groupe de Nicolas Brunner ainsi que dans le groupe de Cyril Branciard de l'Institut Néel à Grenoble. Il a fait sa thèse de doctorat à l'Université d'Auckland en Nouvelle Zélande ainsi qu'à l'ENS Paris, en informatique théorique et en physique sou la correction de Giuseppe Longo et de Cristian Calude.

Il a connu Serguei Brin et assisté à la création de Google... Aujourd'hui, il signe un livre intitulé "Nous sommes les réseaux sociaux". Le chercheur Serge Abiteboul, membre de l'ARCEP, décrypte le fonctionnement des réseaux sociaux.  Serge Abiteboul est une personnalité du monde de l'informatique. Chercheur à l'INRIA et à l'Ecole Normale Supérieure, membre du collège de l'ARCEP (autorité de régulation des télécoms), il a vu naître Google aux Etats-Unis. Co-auteur avec Jean Cattan du livre intitulé "Nous sommes les réseaux sociaux" (éditions Odile Jacob), il explique comment la dérive actuelle des réseaux sociaux est due, selon lui, aux comportements des humains et pas aux outils informatiques. Il en appelle à une prise de conscience et une intervention des pouvoirs publics, dans le fil des récents règlements européens. Une plongée passionnante dans les arcanes des plateformes numériques. Dans cette interview, il raconte aussi la naissance du moteur de recherche, sur le campus de Stanford. 

Nous sommes les réseaux sociaux (ed. Odile Jacob) Les réseaux sociaux – Facebook, Twitter, YouTube, Instagram, TikTok, Reddit, LinkedIn… – ne se substituent pas à nos liens sociaux mais ils les transforment profondément. S'ils s'appuient sur des techniques brillantes de l'informatique, des infrastructures complexes et des modèles économiques aussi astucieux que pernicieux, leur richesse première reste les humains qui construisent ces liens : nous sommes les réseaux sociaux ! Partant de cette conviction, le livre défend l'idée que nous ne pouvons abandonner notre destin à quelques entreprises qui, trop souvent, capturent notre attention et manipulent notre rapport à l'information. Entre la censure excessive et le laisser-faire, une autre voie est possible, plus démocratique, plus participative : les réseaux sociaux seront ce que nous en ferons. Serge Abiteboul , directeur de recherches à l'Inria et à l'ENS Paris et membre du collège de l'Arcep (Autorité de régulation des communications électroniques, des postes et de la distribution de la presse) et Jean Cattan, secrétaire général du Conseil national du numérique sont nos invités.

Fusion nucléaire, géothermie ou encore énergie ambiante : à l'Inria, les chercheur·ses utilisent l'informatique pour concevoir des projets visant à mieux maîtriser les énergies de demain. Cet article a été réalisé dans le cadre d'un partenariat avec Inria. Mise en voix : Sophie Comte  Mixage : Théodore Ravat

Le 17 juin 1972, éclatait l'affaire du Watergate aux États-Unis, l'une des premières affaires d'espionnage aux conséquences retentissantes. 50 ans plus tard, l'espionnage semble faire partie du quotidien, entre données récoltées sur notre téléphone portable, jusqu'aux cyberattaques les plus massives. Quelle est la réalité de la surveillance aujourd'hui ? Comment s'opère-t-elle ? À qui profite le crime ? Comment se protéger ? Sommes-nous condamnés à être espionnés ? Pour en débattre : - Rayna Stamboliyska, experte en Cybersécurité et auteure de La face cachée d'internet, éditions Larousse - Mathieu Cunche, enseignant-chercheur à l'Insa-Lyon et l'Inria, spécialisé dans la protection des données personnelles - Lucien Castex, représentant pour les Affaires publiques à l'Association française pour le nommage Internet en coopération (Afnic) et membre du think tank Renaissance numérique.

Le 17 juin 1972, éclatait l'affaire du Watergate aux États-Unis, l'une des premières affaires d'espionnage aux conséquences retentissantes. 50 ans plus tard, l'espionnage semble faire partie du quotidien, entre données récoltées sur notre téléphone portable, jusqu'aux cyberattaques les plus massives. Quelle est la réalité de la surveillance aujourd'hui ? Comment s'opère-t-elle ? À qui profite le crime ? Comment se protéger ? Sommes-nous condamnés à être espionnés ? Pour en débattre : - Rayna Stamboliyska, experte en Cybersécurité et auteure de La face cachée d'internet, éditions Larousse - Mathieu Cunche, enseignant-chercheur à l'Insa-Lyon et l'Inria, spécialisé dans la protection des données personnelles - Lucien Castex, représentant pour les Affaires publiques à l'Association française pour le nommage Internet en coopération (Afnic) et membre du think tank Renaissance numérique.

Au programme de la 117ème édition de la Contre-Matinale du Média TV, présentée ce mardi 29 mars par Théophile Kouamouo et Cemil Sanli… · Titrologie : Retrouvez la traditionnelle rubrique dans laquelle nous analysons les unes de la presse mainstream et revenons sur leur vision de l'agenda médiatique. Puis, un petit focus sur différents contenus proposés par nos camarades de la galaxie des médias indépendants et alternatifs… · · L'invité : Thomas Dietrich nous parlera des enquêtes du Média, des pressions que l'on reçoit et de l'invisibilisation de nos révélations par les grands médias mainstreams. · Le zapping : Un zapping vidéo qui revient sur les moments forts de nos programmes qui ont marqué l'esprit du collectif d'abonnés du Média qui produit ce zapping chaque semaine par les socios engagés. · La dernière heure : Cemil recevra Gilles Tredan, chercheur au CNRS et Erwan Le Merrer, chercheur à l'INRIA pour discuter de l'algorithme YouTube et de son impact, très très politique, sur la visibilité (ou non) des candidat.e.s à l'élection présidentielle. Vous pouvez retrouver la Contre-matinale en direct audio sur Mixlr : https://mixlr.com/le-media ▶ Soutenez Le Média :

Ingénieur de recherche, chef de projet informatique dédié à la médiation scientifique et à l'innovation pédagogique dans la direction scientifique à l'Inria, spécialiste des impacts environnementaux des technologies numériques, Benjamin Ninassi est également membre du Groupement de service EcoInfo, pour une informatique éco-responsable et de l'INR, l'Institut du Numérique Responsable. Sommaire : * Qu'est ce que l'Inria ? * Qu'est ce que ClassCode ? * Quels sont les éléments à retenir sur les impacts environnementaux du numérique ? * Mooc : objectifs et contenu * Comment en est-il arrivé à s'intéresser au sujet numérique et environnement. * L'écoconception de service numérique * Sensibiliser et former les équipes IT * Comment éviter le greenwashing * Comment faire bouger les lignes dans les grandes organisations * Techno-solutionnisme * Lectures conseillées En savoir plus : * ClassCode : https://pixees.fr/classcode-v2/ * MOOC Impacts environnementaux du numérique : https://www.fun-mooc.fr/fr/cours/impacts-environnementaux-du-numerique/ * Green Patterns (et non "Green Code" comme indiqué dans l'épisode) : https://www.lulu.com/fr/fr/shop/-green-code-lab/green-patterns-manuel-d%C3%A9co-conception-des-logiciels/ebook/product-179y2nnk.html?page=1&pageSize=4

Peu connu du grand public, l'Institut National de Recherche en Informatique et Automatique (INRIA) est au coeur de la recherche publique française en sciences du numérique. Dans cet épisode, je vous propose un entretien exclusif avec son PDG Bruno Sportisse. Créé en 1967, l'INRIA est souvent présenté comme le "CNRS de l'informatique". Il est composé de neuf centres de recherche en France et emploie 3500 scientifiques. Cet institut est à l'origine de nombreuses innovations (notamment en réalité virtuelle, mobilité autonome, cryptographie, robotique, objets connectés, etc.). Il s'est fait connaître du grand public en chapeautant, en 2020, le développement de l'application Stop Covid, devenue Tous Anti-Covid. Dans cet entretien, on évoque plusieurs grands thèmes tels que : le rôle de l'INRIA vis à vis de l'Etat, la souveraineté numérique, la compétition avec les GAFAM et le recrutement de jeunes scientifiques dans un secteur hyper concurrentiel.  (Note : la qualité audio est légèrement altérée en raison du port de masques anti-Covid lors de l'enregistrement)

Pour ce 36e épisode des entretiens Decode Quantum, Fanny Bouton et Olivier Ezratty reçoivent Simon Perdrix qui est directeur de recherche à l'Inria et spécialisé d'une manière générale dans la dimension logicielle et outils logiciels du calcul quantique.

• Qu'est-ce que le Web 3, ce phénomène qui bouscule le monde du numérique ? • Les cryptos et les NFT sont-ils une révolution ? • L'INRIA met au point un système d'exploitation open source pour les objets connectés.

[DECODE Quantum] A la rencontre de Mazyar Mirrahimi, directeur de recherche à l'Inria et en charge de l'équipe Quantic

Au-delà des avions et des voitures, il est un secteur de transport qui est lui aussi assez polluant : le transport maritime. Enfin, peut-être plus pour longtemps grâce à la start up Smart'N'Go et ses solutions technologiques visant à faire des économies de carburant et réduire les émissions polluantes des navires.Derrière Smart'N'Go, on trouve notamment des ingénieurs maritimes, des développeurs, d'anciens marins, des scientifiques, bref, que des professionnels de la mer animés par un but commun : la démocratisation de solutions technologiques pour la marine marchande. Et pour toucher le plus de professionnels possible, la start-up a par ailleurs noué de nombreux partenariats avec la recherche publique comme l'INRIA, CNES et collabore même avec l'agence spatiale européenne pour l'utilisation de ses datas. Car en effet, les solutions proposées par Smart'N'Go se basent en grande partie sur la collecte de données de haute qualité.Dans le détail, l'entreprise propose trois solutions distinctes. Tout d'abord, la solution Manta. Ici, l'idée est de croiser des études hydrodynamiques de chaque navire avec des données de prévisions météo provenant de l'ESA. Ensuite, l'algorithme mis au point par Smart'N'Go calcule la route optimale pour atteindre sa destination. D'après l'entreprise, en choisissant Manta, les navires s'assurent une réduction de 5 à 10% de leur consommation de carburant.Deuxième solution : le Kraken. Ici, l'idée est de calculer très précisément le temps estimé pour arriver à destination tout en réalisant un maximum d'économie. Rien de foncièrement différent avec la solution précédente, si ce n'est pas précision des estimations. Et enfin, la solution Cachalot, qui elle facilite la pesée des navires en détectant automatiquement et très précisément la ligne de flottaison. Vous vous en doutez, ces 3 solutions sont évidemment complémentaires et peuvent s'additionner au sein d'une même plateforme baptisée Lagoon. Pour résumer, en les utilisant toutes ensemble, un navire pourra alors optimiser son trajet, son organisation, et donc réaliser des économies tout en réduisant son empreinte environnementale.Comme vous pouvez le voir, la technologie est un véritable atout pour le secteur du transport maritime qui opère sa transition écologique doucement mais sûrement. A l'instar des voitures, des avions et des trains, certains transporteurs misent même sur de nouveaux modes de propulsion comme l'hydrogène, ou le gaz naturel liquéfié. See acast.com/privacy for privacy and opt-out information.

durée : 00:58:51 - Entendez-vous l'éco ? - par : Tiphaine de Rocquigny, Marguerite Catton - Les débats qui entourent la technologie 5G ne se sont pas taris, malgré le déploiement de la nouvelle génération de technologie réseau mobile dans les grandes villes de France. Que nous promettent la 5G et la 6G comme bouleversements dans nos modes de vie et nos économies ? - réalisation : Anne Depelchin, Philippe Baudouin - invités : Serge Abiteboul Informaticien, membre du Collège de l'Arcep, chercheur à l'ENS Paris et directeur de recherche à l'Inria; Charles Thibout Politiste, chercheur à la Joint European Disruptive Initiative, à l’IRIS et à Paris 1

Guillaume Mandil est enseignant chercheur en science pour l’ingénieur à l’Université Grenoble Alpes, enseignant du master Design of Anthropocene et membre de l’équipe INRIA STEEP depuis 2018. Tu es docteur en génie mécanique et génie industriel. Les sujets abordés - Les travaux menés par l'équipe STEEP au sein de l'INRIA - Écoconception et effet rebond - Le numérique permet d'éviter des pollutions d'autres secteurs - Les limites planétaires et comment cela impacte les services numériques - Qu'enseigner aux étudiants - Comment envisager la fin du numérique ? - Économie circulaire - Comment rester positif, quels conseils donner à celles et ceux qui travaillent dans le secteur du numérique ? - Conseils de lecture En savoir plus : - INRIA / STEEP (Soutenabilité, Territoires, Environnement, Economie et Politique) : https://www.inria.fr/fr/steep - Les besoins artificiels, Razmig Keucheyan https://www.editionsladecouverte.fr/les_besoins_artificiels-9782355221262 - Où atterrir ? Comment s'orienter en politique, Bruno Latour https://www.editionsladecouverte.fr/ou_atterrir_-9782707197009 - Modéliser l'avenir de l'humanité - Heu?reka https://www.youtube.com/watch?v=nAO21ec1lqc - Laurent Mermet : Nous n'avons jamais décollé - une réponse au "Où atterrir?" de Bruno Latour https://www.youtube.com/watch?v=d6ejhMBsjFw

Gilles Dowek est directeur de recherches à l'Inria, enseignant à l'École normale supérieure de Paris-Saclay. Il est également membre du conseil scientifique de la Société Informatique de France ainsi que du Comité national pilote d'éthique du numérique. Il est l'auteur de la chronique Homo sapiens informaticus dans Pour la Science. La crise de la covid19 dans laquelle nous nous trouvons a profondément transformé notre société. Nous discutons dans cet épisode des questions éthiques qu'elle a et continue de soulever, notamment vis à vis des nouvelles technologies numériques. Nous discutons également de questions éthiques plus générales comme notre rapport aux robots par exemple.

Retrouvez le GOOD MORNING FrenchWeb tous les matins dès 6h45 avec Joseph Postec et la rédaction de FrenchWeb.fr pour découvrir les meilleures pratiques et innovation en matière de transformation numérique.J'ai eu le plaisir de m'entretenir avec Anne-Sophie Carrese, Partner chez Elaia.Anne-Sophie nous annonce ce matin un closing du fond Alpha II à hauteur de 30 millions d'euro, en partenariat avec l'Inria.Et en deuxième partie d'émission, nous faisons le point sur l'actualité boursière de l'écosystème numérique avec Antoine Fraysse-Soulier, responsable de l'analyse des marchés chez eToro. Galvanisées par la grande forme des GAFA pendant la crise du coronavirus, nombreuses sont les licornes américaines à prendre le chemin de la Bourse.Focus sur trois d'entre elles : Airbnb, Palantir et Asana.

Les podcasts de l'émission sont disponibles.Au programme de la 74e émission : le sujet principal porte sur le thème de l'informatique avec Sylvie Boldo, directrice de recherche à l'Inria, et Fabien Tarissan chargé de recherche en informatique au CNRS, auteur de l'ouvrage Au cœur des réseaux. Des sciences aux citoyens, Le Pommier, 2019 la première chronique musicale d'Éric Fraudain du site Au Bout Du Fil la chronique « Partager est bon » de Véronique Bonnet, professeure de philosophie et présidente de l'April : présentation et commentaire du texte de Richard Stallman Mettre en application les critères du logiciel libre diverses annonces Pour retrouver toutes les informations concernant l'émission, rendez-vous sur la page dédiée.Sur cette page, vous pouvez commenter les émissions, nous faire des retours pour nous améliorer, ou encore des suggestions. Et même mettre une note sur 5 étoiles si vous le souhaitez. Il est important pour nous d'avoir vos retours car, contrairement par exemple à une conférence, nous n'avons pas un public en face de nous qui peut réagir.Pour connaître les nouvelles concernant l'émission (annonce des podcasts, des émissions à venir, ainsi que des bonus et des annonces en avant-première) inscrivez-vous à la lettre d'actus.

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Leçon inaugurale : Le logiciel, entre l'esprit et la matière.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 OCamlXavier 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

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Leçon inaugurale : Le logiciel, entre l'esprit et la matière.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 OCamlXavier 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

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Leçon inaugurale : Le logiciel, entre l'esprit et la matière.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 OCamlXavier 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

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Leçon inaugurale : Le logiciel, entre l'esprit et la matière.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 OCamlXavier 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

Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Leçon inaugurale : Le logiciel, entre l'esprit et la matière. 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

Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Leçon inaugurale : Le logiciel, entre l'esprit et la matière. 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

Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Leçon inaugurale : Le logiciel, entre l'esprit et la matière. 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

Xavier LeroyCollège de FranceScience du logicielAnnée 2018-2019Leçon inaugurale : Le logiciel, entre l'esprit et la matière.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 OCamlXavier 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