Details of Grant 

EPSRC Reference:	EP/F037368/1
Title:	Behavioural Types for Object-Oriented Languages
Principal Investigator:	Gay, Professor SJ
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	School of Computing Science
Organisation:	University of Glasgow
Scheme:	Standard Research
Starts:	17 January 2008	Ends:	16 July 2008	Value (£):	31,167
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.gla.ac.uk