Détail d'une fiche   Version PDF

CAMBIUM (SR0881NR)

Langages de programmation : systèmes de types, concurrence, preuve de programme

GALLIUM (SR0093AR) →  CAMBIUM


Statut: Décision signée

Responsable : François Pottier

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : A1.1.1. Multi-cœurs, pluri-coeurs , A1.1.3. Modèles memoire , A2.1. Langages de programmation , A2.1.1. Sémantique des langages de programmation , A2.1.3. Programmation orientée objet , A2.1.4. Programmation fonctionnelle , A2.1.6. Programmation concurrente , A2.1.11. Langages de preuve , A2.2. Compilation , A2.2.1. Analyse statique , A2.2.2. Modèles mémoire , A2.2.4. Architectures parallèles , A2.2.5. Environnements d'exécution , A2.4. Méthodes formelles pour vérification, sureté, certification , A2.4.1. Analyse , A2.4.3. Preuves , A2.5.4. Maintenance, évolution , A7.1.2. Algorithmique parallèle , A7.2. Logique , A7.2.2. Déduction automatique , A7.2.3. Assistants de preuve

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : B5.2.3. Aviation , B6.1. Industrie du logiciel , B6.6. Systèmes embarqués , B9.5.1. Informatique

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Preuves et vérification

Période : 01/08/2019 -> 31/12/2024
Dates d'évaluation :

Etablissement(s) de rattachement : COLLEGE DE FRANCE
Laboratoire(s) partenaire(s) : <sans UMR>

CRI : Centre Inria de Paris
Localisation : Centre de recherche Inria de Paris
Code structure Inria : 021155-0

Numéro RNSR : 201923244M
N° de structure Inria: SR0881NR

Présentation

Les travaux de l'équipe visent à améliorer la fiabilité, la sûreté et la sécurité du logiciel en faisant progresser les langages de programmation et les méthodes de vérification formelle de programmes.  La conception, la formalisation et la mise en oeuvre de langages de programmation jouent un rôle central dans les activités de l'équipe.  Les principaux thèmes de recherche sont les systèmes de types et les algorithmes d'inférence de types, la vérification déductive de programmes, le parallélisme à mémoire partagée, et les modèles mémoires faiblement cohérents. L'équipe s'intéresse tout autant aux fondements théoriques qu'aux applications réalistes.


Axes de recherche

L'équipe Cambium conçoit et développe deux grands logiciels de recherche
qui intègrent et font passer dans la pratique bon nombre de ses résultats:
- OCaml, un langage de programmation fonctionnel
  statiquement typé et son implémentation. OCaml est, avec Haskell, un des
  deux langages fonctionnels typés les plus utilisés dans l'industrie
  comme dans la recherche.
- CompCert, un compilateur vérifié pour logiciels
  embarqués critiques. CompCert est le premier compilateur réaliste qui a été
  formellement vérifié à l'aide de méthodes formelles (à savoir l'assistant à
  la démonstration Coq).

 


Relations industrielles et internationales