Behavioural Types for Object-Oriented Languages

The purpose of this proposal is to enable Dr Antonio Ravara, of Instituto Superior Tecnico, Lisbon, to visit Glasgow for six months from 1st January to 30th June 2008. During this visit we will tackle the problem of developing theories and tools to better support the development of distributed communication-based software. This kind of software, in which the structure of the communication between physically separate entities is at least as important as the structure of the computation within those entities, is becoming increasingly significant as the main paradigm for implementing business processes, web services, and service-oriented systems in general. Our aim is to apply type theory, and the technology of compile-time typechecking, to the development of communication-based software.Recent developments in mainstream programming languages have seen an increasing emphasis on the role of types and typechecking---for example, the introduction of generics in Java---butcompile-time-checkable type systems still focus on static descriptions of interfaces to objects and static associations of types with values. However, it is possible for compile-time (or static)typechecking to verify dynamic properties. This has been established by the research of ourselves and others in two areas: behavioural types and session types. Our aim is to unify these areas to produce a powerful type system to support distributed communication-based programming in object-oriented languages.We will draw on a particular style of behavioural type system: non-uniform types for objects. The key idea is to give a static specification of the order in which operations can be carried out on an object: for example, data cannot be extracted from a queue object until some data has been put in. We will also draw on the idea of session types, which are static specifications of the sequence and type of messages exchanged on communication channels. Our aim is to unify these ideas: a communication channel constrained by a session type is a particular kind of non-uniform object, and this observation leads to the idea of using the notation of session types as a convenient notation for more general non-uniform object types. Recent work (including our own) on static typechecking for session types (that is to say, compile-time verification of the specifications that they represent) will enable us to develop effective techniques for the static verification of more general systems of non-uniform objects. Furthermore, we will design a type system which integrates session types and non-uniform object types with the standard concepts of inheritance and subtyping.In order to demonstrate our techniques in practice, we will implement a prototype programming language in which our type system is added to a significant subset of Java.