Behavioural Types for Object-Oriented Languages

本提案的目的是使里斯本高等技术研究所的Antonio Ravara博士能够在2008年1月1日至6月30日期间访问格拉斯哥，为期六个月。在这次访问中，我们将解决发展理论和工具的问题，以更好地支持分布式通信软件的发展。在这种软件中，物理上分离的实体之间的通信结构至少与这些实体中的计算结构一样重要，作为实现业务流程、web服务和面向服务的系统的主要范例，这种软件正变得越来越重要。我们的目标是将类型理论和编译时类型检查技术应用到基于通信的软件开发中。最近主流编程语言的发展越来越强调类型和类型检查的作用——例如，在Java中引入泛型——但是编译时可检查类型系统仍然关注对象接口的静态描述以及类型与值的静态关联。但是，编译时（或静态）类型检查可以验证动态属性。这是我们自己和其他人在两个领域的研究得出的结论：行为类型和会话类型。我们的目标是统一这些领域，以产生一个强大的类型系统，以支持面向对象语言中基于分布式通信的编程。我们将借鉴行为类型系统的一种特殊风格：对象的非统一类型。关键思想是给出对对象执行操作的顺序的静态规范：例如，在将某些数据放入队列对象之前，不能从队列对象中提取数据。我们还将借鉴会话类型的思想，会话类型是在通信通道上交换的消息的序列和类型的静态规范。我们的目标是统一这些想法：受会话类型约束的通信通道是一种特殊的非统一对象，这种观察导致使用会话类型表示法作为更一般的非统一对象类型的方便表示法的想法。最近在会话类型的静态类型检查（也就是说，它们所代表的规范的编译时验证）方面的工作（包括我们自己的工作）将使我们能够开发用于非统一对象的更一般系统的静态验证的有效技术。此外，我们将设计一个类型系统，该系统将会话类型和非统一对象类型与继承和子类型的标准概念集成在一起。为了在实践中演示我们的技术，我们将实现一种原型编程语言，其中我们的类型系统被添加到Java的一个重要子集中。

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.