Research Work Carried Out by Students (Peter00)

Christof Peter.
Expressiveness and Applicability of Process Types.
Dissertation, Institute of Computer Languages, Vienna University of Technology, February 2000.

Abstract:

In this thesis we deal with distributed systems based on calculi of objects that communicate by sending messages. Statically checked process types ensure that each sent message is understood by the receiver. A process type describes also behavior depending on the object's state. The state of an object depends on the previously received messages.

The process type calculus has two important properties: Each object has a unique identifier, and the logical ordering of messages is preserved. While the first property is common in calculi related to the actors model, the second property is not explicitly ensured in most asynchronous calculi.

We examine the properties of process types and the underlaying calculus in comparison to other calculi and their type systems. Especially, we compare them with Vasconcelos' TyCO calculus, a calculus which contains the concepts of Milner's pi-calculus. We give a fully abstract encoding of untyped TyCO programs into our calculus with types. But it is not possible to encode all typed programs in the process type calculus in TyCO; process types are more expressive than TyCO types and support subtyping.

Then we propose higher order process types and a matching relation on them. We present a type checking algorithm and prove that it is sound and complete.

Finally, we describe how a (dynamic) version of process types can be integrated in a practical application like CORBA. The CORBA Interface Definition Language (IDL) is extended with process types. A process type checker is integrated into the CORBA-IDL compiler and activated on each service invocation. All messages that may not be understood by the receiver are discarded instead of being sent.

Dissertation

@PhdThesis{Peter00,
  author  = "Christof Peter",
  title   = "Expressiveness and Applicability of Process Types",
  school  = "{Technische Universit\"at Wien}",
  year    = 2000,
  url     = {http://www.complang.tuwien.ac.at/Dissertationen/peter00.ps.gz},
  address = "Vienna, Austria",
  month   = feb
}