Typing Concurrent Objects and Actors

Fabien Dagnat (1, 2) , Marc Pantel (2, 3) , Matthias Colin (1, 2) , Patrick Sallé (1, 4)

1 ENSEEIHT - Ecole Nationale Supérieure d'Electrotechnique, d'Electronique, d'Informatique, d'Hydraulique et de Télécommunications
2 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
3 Toulouse INP - Institut National Polytechnique (Toulouse)
4 IRIT - Institut de recherche en informatique de Toulouse

As informal methods do little to help their use for concurrent and distributed programming, one of the most challenging current tasks is to build tools based on formal method in order to ease the development of such applications. In this context, we propose precise type systems for concurrent object and actor oriented programming languages. This paper analyzes the type systems that we have developed for realistic languages and presents their benefits and limits. First, it introduces the kernel of an actor language used to describe and validate the proposed technic. Then, the errors we wish to detect are precisely defined. Afterwards, the first type system is defined and its properties are presented. Finally, insights are given on a second more powerful type system, which is the basis of our future work.

Domaines: Génie logiciel [cs.SE]

Fabien Dagnat, Marc Pantel, Matthias Colin, Patrick Sallé. Typing Concurrent Objects and Actors. L'Objet, méthodes formelles pour les objets, 2000. ⟨hal-02061966⟩