{"partition": "head_middle", "source_domain": "www.inria.fr", "digest": "sha1:TPDF2J3WWJGDV5W52YMNDYIASRIYEI6G", "path": "/lustre/fsn1/projects/rech/qgz/uzq54wg/processed_redpajama/base_processing/output/fr/2014-15/000_00037.parquet"}
Inria
Inria Channel
Découvrir Inria, son Actualité, ses activités de Recherche & d'Innovation
Au sommaire
Inria en bref
Michel Cosnard, p-dg d'Inria
Inria en quelques mots
Histoire d'Inria
Ceux qui ont fait Inria
Bilan social
Prix Inria
Ecosystème Inria
Directeurs scientifiques adjoints
Organigramme général
Défis numériques Plan stratégique
Inria et les Alliances
EIT ICT Labs
Le mot de la Directrice des Relations Internationales
Actions dans le monde
Mot de Thierry Priol
Programmes européens
European Research Council EIT ICT Labs
Partenariats académiques
Partenariats industriels
Recrutement & métiers
Mot de Bruno Wierzbicki
Diversité de nos métiers
Boost your code
Chaires Internationales Inria
Focus Prix Inria 2013
Anatole Lécuyer : Prix Inria - Académie des sciences du jeune chercheur
Aujourd'hui responsable de l'équipe Hybrid, Anatole Lécuyer vient de recevoir le Prix lnria - Académie des sciences du jeune chercheur. Personnellement honoré par cette récompense, il estime qu'elle constitue également une sorte de reconnaissance pour ses domaines de recherche, la réalité virtuelle et les interfaces cerveau-ordinateur, encore relativement « jeunes » et mal connus.	Lire la suite
Prix Inria 2013
Jean-Michel Morel : Grand Prix Inria – Académie des Sciences 2013
Il voulait faire de la théorie, il est aujourd'hui passionné par les applications de ses travaux. Il voulait rester dans le monde académique, ses algorithmes sont utilisés par de nombreux industriels. Mais Jean-Michel Morel reste convaincu que sans formalisation mathématique, une découverte ou une théorie n'est pas aboutie ! Fort de cette conviction, il met les mathématiques au service du traitement d'image et du signal pour en expliquer les avancées et en fonder les théories. Avec succès. Il veut partager ses algorithmes librement et a fondé pour cela un journal permettant à chacun d'expérimenter les travaux des autres.	Lire la suite
Pascale Vicat-Blanc : Prix Inria – Académie des sciences – Dassault Systèmes de l'innovation 2013
Fondatrice de l’entreprise Lyatiss, Pascale Vicat-Blanc vient de recevoir le prix de l'innovation lnria - Académie des sciences - Dassault Systèmes. Elle voit dans cette distinction personnelle, une reconnaissance pour son équipe et sa société – et un intérêt pour les jeunes femmes qui pourraient s'en inspirer. Consciente d'être une sorte de role model, elle milite pour le décloisonnement européen des mondes de la recherche, de l'entreprise et de l'investissement.	Lire la suite
Coq récompensé par l’ACM Software System Award
L’ACM (Association for Computing Machinery) annonce que le prix "Software System Award" est décerné à l'équipe de développement du système Coq. Une récompense pour un travail collectif de longue haleine, qu'Inria soutient depuis 30 ans.	Lire la suite
Partenariat CITRIS - Inria - PRIME
Inria, le CITRIS et PRIME ont signé le 12 février 2014 un accord dans le domaine des Smart Cities afin d'accélérer le développement de recherches et d'expérimentations pour résoudre les problèmes relatifs aux grandes aires urbaines. La signature a eu lieu en présence de Michel Cosnard (PDG d'Inria), Sabine Enjalbert (Directrice Générale de l’Agence Régionale de Développement de Paris Île-de-France), Geneviève Fioraso (ministre de l'Enseignement supérieur et de la recherche) et Costas Spanos (directeur du Center for Information Technology Research in the Interest of Society, University of California).	Lire la suite
Rechercher une équipe
Modèle « Équipe-projet »
Chaires d'enseignement et de recherche
Laboratoires communs
Développement technologique à l'institut
Archives - Conférences scientifiques
Programme "Internships"
Equipes associées
Domaines de recherche
Cinq domaines de recherche
Actions d’envergure
Actions exploratoires
Actions de recherche collaboratives
Jeunes chercheurs
Les jeunes chercheurs au coeur de la recherche
Lycéens - Etudiants
Etre doctorant
Etre post-doctorant
Découvrez les sciences du numérique
L'informatique de A à Z
Le patrimoine dans le rétro
Informatique et sciences du numérique
Focus Programme "Equipes associées"
Équipes Associées 2014-2016: appel à projets 2013
Une « Équipe associée » est un projet de recherche commun créé entre une équipe-projet Inria et une équipe de recherche basée à l'étranger. Les deux partenaires définissent conjointement un objectif scientifique, un plan de recherche et un programme d’échanges bilatéraux. Afin de promouvoir et de développer de telles collaborations, en soutenant des projets de recherche d’excellent niveau scientifique, la Direction des relations internationales d’Inria lance chaque année un appel à projets.	Lire la suite
© Inria - Asclepios
Sciences numériques
Leçon inaugurale de Nicholas Ayache
Nicholas Ayache a donné sa leçon inaugurale au Collège de France le jeudi 10 avril 2014 à 18h. Le cours, portant sur l'imagerie médicale computationnelle, s'intitule « Le patient numérique personnalisé : images, médecine, informatique ».	Lire la suite
Partenariats & transfert technologique
Le mot d'Eric Horlait
Rencontres Inria Industrie
Bureau France W3C
iCOMMUNITY
Inria & PME
Institut Carnot Inria
Partenariat bpifrance
Magazine Connect
Calcul haute performance
Secteurs industriels
Aéronautique, défense, spatial, sécurité
Edition de logiciels, systèmes embarqués
Energie, transport, développement durable
Santé, sciences de la vie, biotechnologie
Télécoms, réseaux, multimedia
Focus Voeux 2014 à la French Tech
Fleur Pellerin présente ses voeux à la French Tech
Marie Gallas-Amblard -
Mercredi 29 janvier, la ministre de l’économie numérique et des PME a présenté ses vœux aux acteurs de l’écosystème numérique français rassemblés désormais sous la bannière de la La French Tech. Le logo du label a été présenté représentant en coq en origami pour montrer avec humour une communauté numérique française qui ne se prend pas au sérieux, dixit Fleur Pellerin.	Lire la suite
Les rencontres Inria Industrie
Inria fête en 2014, les 30 ans de sa première création d'entreprises. Depuis l'institut a généré plus de 120 start-up, symboles de sa politique volontariste en matière de transfert des technologies issues de ses équipes de recherche. Lire la suite
Accès direct Actualités scientifiques
Agenda scientifique
Transfert & Innovation
A noter Prix Inria 2013
Et aussi Prix Inria 2013
Favoriser l’accueil des étudiants étrangers
Chaque année, à travers son programme "Internships", Inria reçoit plus d’une centaine d’étudiants du monde entier pour les former par la recherche. L'objectif de ce programme est de renforcer les collaborations scientifiques d'Inria au travers de l'accueil et de la formation par la recherche d'excellents étudiants issus d'Institutions partenaires à l'étranger. Des étudiants de niveau undergraduate, master ou thèse viennent alors passer entre deux et neuf mois, selon leur niveau, auprès d’une équipe de recherche d’Inria. Rencontres avec Michail Zervos et Nadia Khalfa, deux étudiants passionnés qui nous font partager leur expérience réussie et livrent quelques conseils à tous ceux qui pourraient être intéressés par le programme Internships.	Lire la suite
Accès direct Actualités Innovation
Agenda Innovation
Zoom sur Voeux 2014 à la French Tech
Inria & PME - Publication
Innover avec les sciences du numérique - Connect n° 3
Découvrez CONNECT, le magazine à destination des PME qui souhaitent innover avec les sciences du numérique : actualité des STIC, état d'avancée de la Recherche, technologies transférées ou transférables vers le monde industriel, portrait de partenaires issus des équipes de recherche d'Inria avec des PME innovantes, dossiers thématiques, ... N'hésitez pas, CONNECTez-vous !	Lire la suite
Retour sur © Inria / Photo G.Maisonneuve
Rencontre Inria Industrie
Simulation, modélisation et HPC
Le 11 juin dernier, Inria, en partenariat avec Genci et Bpifrance (ex-Oséo), a organisé une Rencontre Inria Industrie dont le sujet "Modélisation, simulation et calcul intensif : de puissants leviers pour la compétitivité des entreprises" a suscité beaucoup d'intérêt...En effet, plus de 200 personnes sont venues assister aux conférences et visiter le showroom présentant les dernières technologies développées par Inria sur la thématique !	Lire la suite
PrésentationActualitésRechercheInnovation
Centre >
Paris - Rocquencourt >
Agenda >
Ecoles CEA-EDF-Inria - Modélisation et vérification d'algorithmes en Coq : une introduction
École CEA-EDF-Inria Modélisation et vérification d'algorithmes en Coq : une introduction
Cette école CEA-EDF-Inria abordera les techniques de base en modélisation et vérification d'algorithmes en Coq. Elle s'adresse aux étudiants, chercheurs ou ingénieurs qui ont une bonne connaissance de la programmation dans un langage conventionnel (C, Java).	Date : 7/06/2010 au 11/06/2010 Lieu : Inria - Rocquencourt bâtiment 1 Organisateurs : Yves Bertot, Pierre Castéran, Pierre Letouzey, Assia Mahboubi Objectifs :Le système Coq fournit un langage de programmation fonctionnelle et un cadre de raisonnement basé sur la logique d'ordre supérieur pour effectuer des preuves sur les programmes. Le pouvoir expressif du langage est tel que l'on peut envisager des preuves sur des notions de mathématiques très avancées (comme le théorème des 4 couleurs) ou des programmes de complexité importante (comme un compilateur pour un noyau significatif du langage C). Dans ce cours, nous aborderons les techniques de base de la programmation dans ce langage et de la démonstration sur les programmes obtenus. Les concepts abordés seront : programmation récursive structurelle, manipulations de listes et d'entiers, démonstration par récurrence, définition récursive de types de données, constructions de filtrage et raisonnement par cas, propriétés inductives.Programme :
Les cours commenceront lundi 7 à 10h, et se termineront vendredi 11 juin à 16h.
Lundi Eléments de programmation fonctionnelle typée : programmation sans effets de bord, filtrage, fonctions anonymes, types prédéfinis simples nombres, booléens, listes, éléments de programmation d'ordre supérieure. Programmation récursive simple sur les nombres et les listes: introduction à la récursion structurelle
Mardi Construction et preuves de formules logiques : quantificateurs et connecteurs logiques, égalité, prédicats prédéfinis sur les nombres et les listes. Démonstration de formules simple en Coq: preuve dirigée par les buts
Vérification de formules logiques simples concernant des programmes Preuves par récurrence sur les nombres et les listes. Nouveaux types de données et nouveau principes de raisonnement associés
Prédicats inductifs et introduction aux types dépendants. Preuves par récurrence sur les prédicats inductifs. Fonctions à type dépendant, filtrage avec type dépendant
Combinaisons de types de données et de propriétés logiques Types portant des informations logiques Récursion généralisée
Mots-clés : Méthodes formelles
Assistant de preuve Coq
Algorithmes
Pages web de l'école
Bernard BIGOT (CEA)
Yves BAMBERGER (EDF)
Michel COSNARD (Inria)
Comité directeur Didier BESNARD (CEA/DIF)
Christian CHAULIAC (CEA/DEN)
Eric CANCES (Inria)
Eric LORENTZ (EDF)
Bruno SCHEURER (CEA/DIF)
Francesco ZAPPA NARDELLI (Inria)
Le site web de nos partenaires :
SMAI
Les écoles CEA-EDF-Inria s'adressent à tous les scientifiques dans le domaine des mathématiques appliquées et de l'informatique. Elles proposent des cours et des exposés thématiques et sont organisées tout au long de l'année, principalement pour Inria. Certaines écoles ont lieu l'été et sont organisées par le CEA.Écoles CEA-EDF-Inria 2010
13-12 décembre - Homogénéisation périodique et stochastique, aspects théoriques et numériques
27-30 septembre - Simulation of hybrid dynamical systems and applications to molecular dynamics
Siège et centres de recherche Inria
Bordeaux - Sud-Ouest
Grenoble - Rhône-Alpes
Lille - Nord Europe
Nancy - Grand Est
Paris - Rocquencourt
Rennes - Bretagne Atlantique
Saclay - Île-de-France
Sophia Antipolis - Méditerranée
Rapports d'activité - RAweb
Archive ouverte - HAL-Inria
Fuscia, bureau d'accueil
Logo Inria
Inria Alumni
Inriality
Interstices
Inria sur Canal-U