Behavioural Types for Object-Oriented Languages

这项建议的目的是使里斯本高等技术学院的Antonio Ravara博士能够从2008年1月1日至6月30日访问格拉斯哥六个月。在这次访问中，我们将解决开发理论和工具以更好地支持基于分布式通信的软件开发的问题。在这种软件中，物理上分离的实体之间的通信结构至少与这些实体内的计算结构一样重要，作为实现业务流程、网络服务和面向服务的系统的主要范例，这种软件正变得越来越重要。我们的目标是将类型理论和编译时类型检查技术应用到基于通信的软件开发中。最近主流编程语言的发展越来越重视类型和类型检查的作用-例如，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.