Action Miró/Mirho : Systèmes à Objets, Types et Prototypes : Sémantique et Validation

Luigi Liquori 1, 2 Dominique Colnet 1 Joelle Despeyroux 1
1 MIRHO - Objects, types and prototypes : semantics and validation
CRISAM - Inria Sophia Antipolis - Méditerranée , UHP - Université Henri Poincaré - Nancy 1, Université Nancy 2, INPL - Institut National Polytechnique de Lorraine, CNRS - Centre National de la Recherche Scientifique : UMR7503
Résumé : Johachim Miró est, à notre humble avis, un grand peintre "à objets" ; en fait, ses tableaux de la période 1940-1960 sont basés sur l'utilisation de nombreux objets géométriques : points, points colorés, carrés, cercles, fenêtres, lignes, courbes, etc. Tous ces éléments sont très chers aux amateurs de la programmation par objets. On peut même aller jusqu'à imaginer que ce peintre, qui s'est installé en France à Montmartre au début des années 50, a certainement inspiré les concepteurs de Simula, de SmallTalk, et la communauté d'informaticiens qui ont étudié les aspects théoriques du paradigme à objets.
Objectifs généraux de Miró/Mirho
Les langages à objets ont acquis une importance prépondérante dans les applications informatiques à grande échelle. Cette utilisation a rendu nécessaire l'étude formelle de ces langages 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 une plus grande expressivité avec une sécurité et efficacité d'utilisation.
L'action explore 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, et s'intéresse à 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.
En complément de ces axes de recherche principaux, nous étudions des théories typées, dans la recherche de nouveaux systèmes améliorant l'activité de la preuve formelle, et dans la compilation efficace des langages de programmation à objets.
Notre programme de recherche se focalise essentiellement sur les axes suivants :
- l'étude, la définition et l'implantation certifiée d'un langage de programmation à classes (et de son compilateur), appelé SmallTalk2K, et d'un langage à prototypes (cad à objets purs), appelé FunTalk (et d'un interprète et d'un compilateur), langage intermédiaire du compilateur de SmallTalk2K ;
- l'étude de l'efficacité et de la sûreté des langages à objets et notamment d'\textit{Eiffel} (et ses évolutions) et de son compilateur SmallEiffel ;
- l'étude de systèmes de types pour les langages à objets et pour les assistants de preuves; la réécriture et les calculs formels (lambda, varsigma, rho, pi, ...) comme base des langages de programmation à objets, fonctionnels et concurrents ;
- l'étude du système d'exploitation Isaac et de son langage propriétaire à prototypes Lisaac.
Type de document :
Autre publication
Guide de lecture
La structure du document est la suivante\,: la section 3 présente les.. 2001
Liste complète des métadonnées

https://hal.inria.fr/hal-01151339
Contributeur : Luigi Liquori <>
Soumis le : mercredi 13 mai 2015 - 14:51:15
Dernière modification le : samedi 27 janvier 2018 - 01:30:57
Document(s) archivé(s) le : mercredi 19 avril 2017 - 22:31:53

Fichier

2002-mirov1.3-epi-proposal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01151339, version 1

Collections

Citation

Luigi Liquori, Dominique Colnet, Joelle Despeyroux. Action Miró/Mirho : Systèmes à Objets, Types et Prototypes : Sémantique et Validation. Guide de lecture
La structure du document est la suivante\,: la section 3 présente les.. 2001. 〈hal-01151339〉

Partager

Métriques

Consultations de la notice

311

Téléchargements de fichiers

49