Détail d'une fiche   Version PDF

MIRHO (SR0360CR)

Systèmes à objets, types et prototypes : sémantique et validation

CERTILAB (SR0328GR) →  MIRHO


Statut: Terminée

Responsable : Luigi Liquori

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : Aucun mot-clé.

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : Aucun mot-clé.

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Algorithmique, calcul certifié et cryptographie

Période : 01/01/2003 -> 31/12/2003
Dates d'évaluation :

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

CRI : Centre Inria d'Université Côte d'Azur
Localisation : Centre Inria d'Université Côte d'Azur
Code structure Inria :

Numéro RNSR : 200321490A
N° de structure Inria: SR0360CR

Présentation

L'un des objectifs de Miro consiste à explorer la possibilité de "concilier" la programmation à objets et la programmation fonctionnelle, tout en gardant l'esprit de l'une et l'élégance mathématique de l'autre.

Les langages à objets ont acquis une importance prépondérante dans les applications informatiques à grande échelle. Cette utilisation a rendu nécessaire l'étude de ces langages tant d'un point de vue formel que pratique, pour à la fois mieux en cerner les caractéristiques fondamentales et aussi pour pouvoir définir de nouveaux langages à objets et concurrents, capables de combiner expressivité avec sécurité d'utilisation et efficacité. C'est dans ce dernier cadre que notre recherche se situe.

Nous étudions la théorie des types, la recherche de nouveaux systèmes améliorant l'activité de la preuve formelle, la compilation et l'exécution efficace des langages de programmation à objets, et les systèmes d'exploitation à objets. Nous nous intéressons à la certification des outils développés autour de ces langages (interprètes, compilateurs, ...), avec comme assistant à la preuve privilégié, le système Coq.


Axes de recherche

Ainsi, notre programme de recherche se focalise donc essentiellement sur les trois points suivants :
  • l'étude, la définition, et l'implantation certifiée d'un langage de programmation à classes, appelé SmallTalk2K, et d'un langage à prototypes, appelé FunTalk, langage intermédiaire du compilateur de SmallTalk2K ;
  • l'étude de l'efficacité et de la sûreté (allocation et gestion mémoire, prédiction de types et liaison dynamique) des systèmes à objets, notamment du compilateur SmallEiffel et du système d'exploitation Isaac ;
  • la théorie des types pour les langages à objets et pour les assistants de preuves, le logiciel certifié, la réécriture et les calculs formels (lambda, pi, sigma, rho, join, ...) à la base des langages de programmation à objets, fonctionnels et concurrents.

Relations industrielles et internationales

ENS Lyon, Un. Turin, Un. Udine, Mc. Gill, ANU,IST/types, FSF