Action Miró/Mirho
Luigi Liquori, Dominique Colnet, Joëlle Despeyroux · 2001
Johachim Miro est, notre humble avis, un grand peintre a ; en fait, ses tableaux de la periode 1940-1960 sont bases sur l'utilisation de nombreux objets geometriques : points, points colores, carres, cercles, fenetres, lignes, courbes, etc. Tous ces elements sont tres chers aux amateurs de la programmation par objets. On peut meme aller jusqu'a imaginer que ce peintre, qui s'est installe en France Montmartre au debut des annees 50, certainement inspire les concepteurs de Simula, de SmallTalk, et la communaute d'informaticiens qui ont etudie les aspects theoriques du paradigme objets. Objectifs generaux de Miro/Mirho Les langages objets ont acquis une importance preponderante dans les applications informatiques grande echelle. Cette utilisation rendu necessaire l'etude formelle de ces langages pour la fois mieux en cerner les caracteristiques fondamentales et aussi pour pouvoir definir de nouveaux langages objets et concurrents, capables de combiner une plus grande expressivite avec une securite et efficacite d'utilisation. L'action explore la possibilite de concilier'' la programmation objets et la programmation fonctionnelle, tout en gardant l'esprit de l'une et l'elegance mathematique de l'autre, et s'interesse la certification des outils developpes autour de ces langages (interpretes, compilateurs, ...), avec comme assistant la preuve privilegie le systeme Coq. En complement de ces axes de recherche principaux, nous etudions des theories typees, dans la recherche de nouveaux systemes ameliorant l'activite 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'etude, la definition et l'implantation certifiee d'un langage de programmation classes (et de son compilateur), appele SmallTalk2K, et d'un langage prototypes (cad objets purs), appele FunTalk (et d'un interprete et d'un compilateur), langage intermediaire du compilateur de SmallTalk2K ; - l'etude de l'efficacite et de la surete des langages objets et notamment d'\textit{Eiffel} (et ses evolutions) et de son compilateur SmallEiffel ; - l'etude de systemes de types pour les langages objets et pour les assistants de preuves; la reecriture et les calculs formels (lambda, varsigma, rho, pi, ...) comme base des langages de programmation objets, fonctionnels et concurrents ; - l'etude du systeme d'exploitation Isaac et de son langage proprietaire prototypes Lisaac.