MIRHO : Objects, types and prototypes : semantics and validation

About the team : Team site (french) Activity report Research reports and theses Theme : 2 Software engineering and symbolic computing Sophia Antipolis research unit

MIRHO has been dissolved on 12/31/2003

Team Presentation

LORIA and Sophia Antipolis joint and bilocated team

One of the goals of Miro consists in investigating the possibility to "reconcile" object-oriented programming and functional programming while keeping the spirit of the former and the elegance of the latter.

Object-oriented languages have become a major trend in large scale computer applications. This has made it necessary to study these languages both from a theoretical and a practical point of view, in order to better exhibit their fundamental characteristics and at the same time define new object-oriented and concurrent languages able to combine expressiveness to security and efficiency. Our research belongs to this context.

We study type theory, new systems improving formal proofs, efficient compilation and execution of object-oriented languages, and object-oriented operating systems. We are interested in certifying the tools developed for these languages (interpreters, compilers, ...), using the Coq system as a favorite proof assistant.

Research themes

Hence, our research program focuses mainly on the three following points :

• the study, definition and certified implementation of a class-based language called SmallTalk2K, and of a prototype-based language called FunTalk, used as intermediate language for the SmallTalk2K compiler, defined later in this document ;
• the study of object-oriented systems security and efficiency, especially for the SmallEiffel compiler and the Isaac operating system, defined later in this document ;
• type theory for object-oriented languages and for proof assistants, certified software, rewriting and formal calculi (lambda, pi, varsigma, rho, dots) which are the foundation of object-oriented, functional and concurrent languages.

International and industrial relations

ENSL, U. Turin, U. Udine, Mc. Gill, ANU, FSF

Scientific leader

Luigi LIQUORI
+33 3 83 58 17 03
Luigi.Liquori@inria.fr
Secretary : +33 3 83 58 30 54