abstracts

2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 2000 | 1999 | 1998 | 1997 | 1996 | 1995 | 1994 | 1993 | 1992

A recent trend in programming language research is to use behav- ioral type theory to ensure various correctness properties of large- scale, communication-intensive systems. Behavioral types encompass concepts such as interfaces, communication protocols, contracts, and choreography. The successful application of behavioral types requires a solid understanding of several practical aspects, from their represen- tation in a concrete programming language, to their integration with other programming constructs such as methods and functions, to de- sign and monitoring methodologies that take behaviors into account. This survey provides an overview of the state of the art of these aspects, which we summarize as the pragmatics of behavioral types.

Session types describe the structure of protocols from the point of view of each participating channel. In particular, the types describe the type of communicated values, and also the dynamic alternation of input and output actions on the same channel, by which a protocol can be statically verified. Crucial to any term language with session types is the notion of linearity, which guarantees that channels exhibit exactly the behaviour prescribed by their type. We relax the condition of linearity to that of affinity, by which channels exhibit at most the behaviour prescribed by their types. This more liberal setting allows us to incorporate an elegant error handling mechanism which simplifies and improves related works on exceptions. Moreover, our treatment does not affect the progress properties of the language: sessions never get stuck.

Session type systems are an effective tool to prove that communicating programs do not go wrong, ensuring that the participants of a session follow the protocols described by the types. In a previous work we introduced a typing discipline for the analysis of progress in binary sessions. In this paper we generalize the approach to multiparty sessions following the conversation type approach, while strengthening progress to liveness. We combine the usual session-like fidelity analysis with the liveness analysis and devise an original treatment of recursive types allowing us to address challenging configurations that are out of the reach of existing approaches.

We present SePi, a concurrent programming language based on the monadic pi-calculus, where interaction is governed by linearly refined session types. On top of the core calculus and type system, and in order to facilitate programming, we introduce a number of abbreviations and derived constructs. This paper provides a brief introduction to the language.

A linguagem intermédia MIL é apropriada para programação baixo nível de aplicações concorrentes com uso de memória partilhada. O seu sistema de tipos polimórfico garante que programas MIL bem tipificados não possuem condições de corrida nem impasses. A primeira propriedade é conseguida através da imposição de uma disciplina no uso de trincos através de tipos singulares; a segunda é alcançada através de anotações polimórficas sobre a ordem pela qual os trincos são fechados em cada bloco de código. O sistema de tipos recusa programas cujos fios de execução dependam ciclicamente uns dos outros no fecho de trincos. No entanto, a introdução de anotações sobre trincos pode introduzir uma complexidade desnecessária no processo de geração de código. Este artigo propõe um algoritmo para inferir as anotações polimórficas sobre trincos. A inferência é feita através da recolha de restrições locais sobre a ordem pela qual os trincos são fechados em cada bloco de código. As restrições são passadas a um SMT que averigua a sua consistência. Implementámos o algoritmo e experimentámo-lo extensivamente em programas MIL, nomeadamente em código de alguma dimensão obtido da compilação de uma linguagem de objetos concorrentes.

Message Passing Interface (MPI) é a infraestrutura padrão de troca de mensagens para o desenvolvimento de aplicações paralelas. Duas décadas após a primeira versão da sua especificação, aplicações baseadas em MPI correm hoje rotineiramente em super computadores e em grupos de computadores. Estas aplicações, escritas em C ou Fortran, exibem intrincados comportamentos, o que torna difícil verificar estaticamente propriedades importantes, tais como a ausência de corridas ou impasses. A abordagem que apresentamos neste artigo pretende validar programas escritos na linguagem C utilizando primitivas de comunicação MPI. Encontra-se dividida em duas linhas orientadoras. Definimos um protocolo de comunicação numa linguagem que criámos para o efeito, inspirada nos tipos de sessão. Este protocolo é depois traduzido para a linguagem de um verificador de software paraC, o VCC. Anotamos depois o programa C com asserções que levam o verificador a provar ou a refutar a conformidade do programa com o protocolo. Grande parte das anotações necessárias são introduzidas automaticamente por um anotador que desenvolvemos. Até à data conseguimos validar com sucesso vários programas que atestam o sucesso da nossa abordagem.

We present a type system for the analysis of progress in session-based communication centred systems. Our development is carried out in a minimal setting considering classic (binary) sessions, but building on and generalising previous work on progress analysis in the context of conversation types. Our contributions aim at underpinning forthcoming works on progress for session-typed systems, so as to support richer verification procedures based on a more foundational approach. Although this work does not target expressiveness, our approach already addresses challenging scenarios which are unaccounted for elsewhere in the literature, in particular systems that interleave communications on received session channels.

Programming languages and systems need to provide for advanced parallel programming coordination techniques, to draw performance out of parallel machines. Some proposals, notably phasers, relax barrier synchronisation to improve expressiveness. These constructs exhibit intricate semantics and most of them are only described informally, which hinders their understanding. We present an operational semantics and a type system for a fork/join programming model equipped with relaxed barriers. Our proposal allows for a precise control over the maximum number of synchronisation steps each task can be ahead of others; the type system enforces a deadlock-free usage of multiple barriers, establishing the properties of subject reduction and progress.

We give a formal account of SSCC, a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocols that services follow when invoked (conversation). The calculus includes primitives for defining and invoking services, for isolating conversations (called sessions) among clients and servers, and for orchestrating services. The calculus is equipped with a reduction and a labeled transition semantics related by an equivalence result. SSCC provides a good trade-off between expressive power for modeling and simplicity for analysis. We assess the expressive power by modeling van der Aalst workflow patterns and an automotive case study from the European project Sensoria. For analysis, we present a simple type system ensuring compatibility of client and service protocols. We also study the behavioral theory of the calculus, highlighting some axioms that capture the behavior of the different primitives. As a final application of the theory, we define and prove correct some program transformations. These allow to start modeling a system from a typical UML Sequence Diagram, and then transform the specification to match the service-oriented programming style, thus simplifying its implementation using web services technology.

We present a type system based on session types that works on a conventional pi calculus. Types are equipped with a constructor that describes the two ends of a single communication channel, this being the only type available for describing the behaviour of channels. Session types, in turn, describe the behaviour of each individual channel end, as usual. A novel notion of typing context split allows for typing processes not typable with extant type systems. We show that our system guarantees that typed processes do not engage in races for linear resources. We assess the expressiveness of type system by providing three distinct encodings - from the pi calculus with polarised variables, from the pi calculus with accept and request primitives, and from the linear pi calculus - into our system. For each language we present operational and typing correspondences, showing that our system effectively subsumes foregoing works on linear and session types. In the case of the linear pi calculus we also provide a completeness result.

The Message Passing Interface (MPI) is the de facto standard message-passing infras- tructure for developing parallel applications. Two decades after the first version of the library specification, MPI-based applications are nowadays routinely deployed on super and cluster computers. These applications, written in C or Fortran, exhibit intricate mes- sage passing behaviours, making it hard to statically verify important properties such as the absence of deadlocks. Our work builds on session types, a theory for describing proto- cols that provides for correct-by-construction guarantees in this regard. We annotate MPI primitives and C code with session type contracts, written in the language of a software verifier for C. Annotated code is then checked for correctness with the software verifier. We present preliminary results and discuss the challenges that lie ahead for verifying realistic MPI program compliance against session types.

Communication protocols in distributed systems often specify the roles of the parties involved in the communications, namely for enforcing security policies or task assignment purposes. Ensuring that implementations follow role-based protocol specifications is challenging, especially in scenarios found, e.g., in business processes and web applications, where multiple peers are involved, single peers impersonate several roles, or single roles are carried out by several peers. We present a type-based analysis for statically verifying role-based multi-party interactions, based on a simple pi-calculus model and prior work on conversation types. Our main result ensures that well-typed systems follow the role-based protocols prescribed by the types, including systems where roles are flexibly assigned to processes.

Our proposal for verification of MPI programs is based on session types. The methodology considers the specification of a global interaction protocol among multiple participants, from which we can derive an endpoint protocol for each individual participant, e.g., as in Scribble. A well-formed protocol can be verified in polynomial time and ensures type safety, communication safety, and deadlock freedom. The idea is that we can ensure these properties for an MPI program by verifying conformance of the program against a given session type specification. This contrasts with other state-of-the-art methodologies considered for MPI, like model checking or symbolic execution, that require program-level analysis for all properties of interest, and inherently lead to a state-explosion problem as the number of participants grows.

We propose a process algebra, the Algebra of Behavioural Types. A type is a higher-order labelled transition system that characterises all possible life cycles of a concurrent object. States represent interfaces of objects; state transitions model the dynamic change of object interfaces. Moreover, a type provides an internal view of the objects that inhabit it: a synchronous one, since transitions correspond to message reception. To capture this internal view of objects we define a notion of bisimulation, strong on labels and weak on silent actions. We study several algebraic laws and obtain completeness results for finite types.

Session types capture precise protocol structure in concurrent programming, but do not specify properties of the exchanged values beyond their basic type. Refinement types are a form of dependent types that can address this limitation, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. We present a pi calculus with assume and assert operations, typed using a session discipline that incorporates refinement formulae written in a fragment of Multiplicative Linear Logic. Our original combination of session and refinement types together with the well established benefits of linearity allow very fine-grained specifications of communication protocols in which refinement formulae are treated as logical resources rather than persistent truths.

We present a reconstruction of session types in a linear pi calculus where types are qualified as linear or unrestricted. Linearly qualified communication channels are guaranteed to occur in exactly one thread, possibly multiple times; unrestricted (or shared) channels may appear in an unbounded number of threads. In our language each channel is characterised by two distinct variables, one used for reading, the other for writing; scope restriction binds together two variables, thus establishing the correspondence between the two ends of a same channel. This mechanism allows a precise control of resources via a conventional linear type system. Furthermore, the uniform treatment of linear and shared channels leads to a surprisingly simply theory which, in addition, extends typability when compared to traditional systems for session types. We build the language gradually, starting from simple input/output, then adding recursive types, replication and finally choice. We also present an algorithmic type checking system.

We discuss session types independently of any programming language. We then embody the notion in languages from three different paradigms: the pi calculus, a functional language, and an object-oriented language.

As software tends to be increasingly concurrent, the paradigm of message passing is becoming more prominent in computing. The language Erlang offers an intuitive and industry-tested implementation of process-oriented programming, combining pattern-matching with message mailboxes, resulting in concise, elegant programs. However, it lacks a successful static verification mechanism that ensures safety and determinism of communications with respect to well-defined specifications. We present a session typing system for a featherweight Erlang calculus that encompasses the main communication abilities of the language. In this system, structured types are used to govern the interaction of Erlang processes, ensuring that their behaviour is safe with respect to a defined protocol. The expected properties of subject reduction and type safety are established.

Core calculi have been adopted in the Sensoria project with three main aims. First of all, they have been used to clarify and formally define the basic concepts that characterize the Sensoria approach to the modeling of service-oriented applications. In second place, they are formal models on which the Sensoria analysis techniques have been developed. Finally, they have been used to drive the implementation of the prototypes of the Sensoria languages for programming actual service-based systems. This chapter reports about the Sensoria core calculi presenting their syntax and intuitive semantics, and describing their main features by means of a common running example, namely a Credit Request scenario taken from the Sensoria Finance case study.

Dependent type systems allow semantic properties to be expressed in types that carry important information about program values. The type systems in mainstream languages such as Java are effective but have a limited expressive power. We propose to extend a simple Java-like language with indexed types, a form of dependent types defined on index expressions that can statically detect many programming errors. Index types take the form of type annotations in the generics style, so as to express semantic properties in a fashion familiar to object-oriented programmers. For example, Polynomial<3> is an instance of Polynomial, where \lstinline|degree| has type nat, which is the type of all polynomials of some degree. Expressions in index types currently represent integer values only. Index types may be associated with class definitions, and may be used to constrain base types in fields or local variables, in arguments to methods or in return types. As opposed to conventional types, indexed types may change over a program lifetime. We discuss introducing indirection into type environments to provide support to type check references to mutable objects.

There is often a sort of a protocol associated to each class, stating when and how certain methods should be called. Given that this protocol is, if at all, described in the documentation accompanying the class, current mainstream object-oriented languages cannot provide for the verification of client code adherence against the sought class behaviour. We have defined a class-based concurrent object-oriented language that formalises such protocols in the form of usage types. Usage types are attached to class definitions, allowing for the specification of (1) the available methods, (2) the tests clients must perform on the result of methods, and (3) the object status - linear or shared - all of which depend on the object's state. Our work extends the recent approach on modular session types by eliminating channel operations, and defining the method call as the single communication primitive in both sequential and concurrent settings. In contrast to previous works, we define a single category for objects, instead of distinct categories for linear and for shared objects, and let linear objects evolve into shared ones. We introduce a standard sync qualifier to prevent thread interference in certain operations on shared objects. We formalise the language syntax, the operational semantics, and a type system that enforces by static typing that methods are called only when available, and by a single client if so specified in the usage type. We illustrate the language via a complete example.

X10 is a modern language built from the ground up to handle future parallel systems, from multicore machines to cluster configurations. We take a closer look at a pair of synchronisation mechanisms: finish and clocks. The former waits for the termination of parallel computations, the latter allow multiple concurrent activities to wait for each other at certain points in time. In order to better understand these concepts we study a type system for a stripped down version of X10. The main result assures that well typed programs do not run into the errors identified in the X10 language reference, namely the ClockUseException. The study will open, we hope, doors to a more flexible utilisation of clocks in the X10 language.

Even though generics became quite popular in mainstream object-oriented (OO) languages, approaches for checking at runtime the conformance of such programs against formal specifications still lack appropriate support. In order to overcome this limitation within ConGu, a tool-based approach we have been developing to support runtime conformance checking of Java programs against algebraic specifications, we recently proposed a notion of refinement mapping that allows to define correspondences between parametric specifications and generic classes. Based on such mappings, we also put forward a notion of conformance between the two concepts. In this paper we present how the new notion of conformance is supported by version 2 of the ConGu tool.

We present a reconstruction of session types in a conventional pi calculus where types are qualified as linear or unrestricted. Linearly typed communication channels are guaranteed to occur in exactly one thread, possibly multiple times. We equip types with a constructor that denotes the two ends of a same communication channel. In order to assess the flexibility of the new type system, we provide three distinct encodings (from the linear lambda calculus, from the linear pi calculus, and from the pi calculus with polarized variables) into our system. For each language we present operational and typing correspondences, showing that our system effectively subsumes the linear pi calculus as well as foregoing works on session types.

We present a simple and intuitive type system for a variant of the pi calculus with sessions where typable processes are guaranteed to be exempt from runtime errors. The type system, meant to type programs, cannot be directly used to type the runtime language. Hence, type-safety cannot be proved directly, via Subject Reduction. Instead we define a different language enjoying Subject Reduction and prove our result by suitable correspondences between the two languages. The exercise shows that polarities, now widely used in binary session types, are justified solely by technical reasons, and need not be exposed to programmers neither in the operational semantics nor in the type system.

Session types support a type-theoretic formulation of structured patterns of communication, so that the communication behaviour of agents in a distributed system can be verified by static type checking. Applications include network protocols, business processes, and operating system services. In this paper we define a multithreaded functional language with session types, which unifies, simplifies and extends previous work. There are four main contributions. First: an operational semantics with buffered channels, instead of the synchronous communication of previous work. Second: we prove that the session type of a channel gives an upper bound on the necessary size of the buffer. Third: session types are manipulated by means of the standard structures of a linear type theory, rather than by means of new forms of typing judgement. Fourth: a notion of subtyping, including the standard subtyping relation for session types (imported into the functional setting), and a novel form of subtyping between standard and linear function types which allows the typechecker to handle linear types conveniently. Our new approach significantly simplifies session types in the functional setting, clarifies their essential features, and provides a secure foundation for language developments such as polymorphism and object-orientation.

Modular Session Types for Distributed Object-Oriented Programming

Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type-checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be modularized, i.e., partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestates supporting non-uniform objects, i.e., objects that dynamically change the set of available methods. We define syntax, operational semantics, a sound type system, and a correct and complete type checking algorithm for a small distributed class-based object-oriented language. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state. We also describe a prototype implementation as an extension of Java.

We previously developed a polymorphic type system and a type checker for a multithreaded lock-based polymorphic typed assembly language (MIL) that ensures that well-typed programs do not encounter race conditions. This paper extends such work by taking into consideration deadlocks. The extended type system verifies that locks are acquired in the proper order. Towards this end we require a language with annotations that specify the locking order. Rather than asking the programmer (or the compiler's backend) to specifically annotate each newly introduced lock, we present an algorithm to infer the annotations. The result is a type checker whose input language is non-decorated as before, but that further checks that programs are exempt from deadlocks.

The construction of reliable concurrent and distributed systems is an extremely difficult endeavour. For complex systems, it requires modular development strategies based on precise interface specifications that allow the various modules to interact properly. In this extended abstract we are concerned with message passing systems where partners engage in long and complex interactions, as opposed to, say, remote procedure calls composed of a pair of simple interactions. Session types allow for the description of continuous series of interactions between several partners. In the simpler case, they detail protocols between two partners; recently the original setting was widened to encompass multiple partners. In this paper we deal with binary sessions only. Through a running example we visit session types and a functional concurrent language equipped with buffered semantics. Apart from the traditional ``well typed programs do not go wrong'', the semantics proposed allows for two extra interesting results: the ability to predict the required buffer size, and that of anticipating an output with respect to an input operation.

Although generics became quite popular in mainstream object-oriented languages and several specification languages exist that support the description of generic components, conformance relations between object-oriented programs and formal specifications that have been established so far do not address genericity. In this paper we propose a notion of refinement mapping that allows to define correspondences between parameterized specifications and generic Java classes. Based on such mappings, we put forward a conformance notion useful for the extension of ConGu, a tool-based approach we have been developing to support runtime conformance checking of Java programs against algebraic specifications, so that it becomes applicable to a more comprehensive range of situations, namely those that appear in the context of a typical Algorithms and Data Structures course.

We present a reconstruction of session types in a linear pi calculus where types are qualified as linear or unrestricted. Linearly qualified communication channels are guaranteed to occur in exactly one thread, possibly multiple times; unrestricted (or shared) channels may appear in an unbounded number of threads. In our language each channel is characterised by two distinct variables, one used for reading, the other for writing; scope restriction binds together two variables, thus establishing the correspondence between the two ends of a same channel. This mechanism allows a precise control of resources via a conventional linear type system. Furthermore, the uniform treatment of linear and shared channels leads to a surprisingly simply theory which, in addition, extends typability when compared to traditional systems for session types. We build the language gradually, starting from simple input/output, then adding recursive types, replication and finally choice. We also present an algorithmic type checking system.

Session-Based Compilation Framework for Multicore Programming

This paper outlines a general picture of our ongoing work under EU Mobius and Sensoria projects on a type-based compilation and execution framework for a class of multicore CPUs. Our focus is to harness the power of concurrency and asynchrony in one of the major forms of multicore CPUs based on distributed, non-coherent memory, through the use of type-directed compilation. The key idea is to regard explicit asynchronous data transfer among local caches as typed communication among processes. By typing imperative processes with a variant of session types, we obtain both type-safe and efficient compilation into processes distributed over multiple cores with local memories.

We extend a previous work on a multithreaded typed assembly language (MIL) targeted at shared memory multiprocessors, and describe the design of a type-preserving compiler from the pi-calculus into MIL. The language enforces a policy on lock usage through a typing system that also ensures race-freedom for typable programs, while allowing for typing various important concurrency patterns. Our translation to MIL generates code that is then linked to a library supporting a generic unbounded buffer monitor, variant of Hoare's bounded buffer monitor, entirely written in MIL. Such a monitor shields client code (the pi-calculus compiler in particular) from the hazardous task of direct lock manipulation, while allowing for the representation of pi-calculus channels. The compiler produces type correct MIL pgenerating low-contention cooperative multithreaded programs.

In this paper, we outline a general picture of our ongoing work on a compilation and execution framework for a class of multicore CPUs. Our focus is to harness the power of concurrency and asynchrony in one of the major forms of multicore CPUs based on distributed, noncoherent memory, using the well-known technology of type-directed compilation. The key idea is to regard explicit asynchronous data transfer among local caches as typed communication among processes. By typing imperative processes with a variant of session types, we obtain both type-safe and efficient compilation into processes distributed over multiple cores with local memories.

We define a small class-based object-oriented language in which the availability of methods depends on an object's abstract state: objects' interfaces are dynamic. Each class has a session type which provides a global specification of the availability of methods in each state. A key feature is that the abstract state of an object may depend on the result of a method whose return type is an enumeration. Static typing guarantees that methods are only called when they are available. We present both a type system, in which the typing of a method specifies pre- and post-conditions for its object's state, and a typechecking algorithm, which infers the pre- and post-conditions from the session type, and prove type safety results. Inheritance is included; a subtyping relation on session types, related to that found in previous literature, characterizes the relationship between method availability in a subclass and in its superclass. We illustrate the language and its type system with example based on a Java-style iterator and a hierarchy of classes for accessing files, and conclude by outlining several ways in which our theory can be extended towards more practical languages.
Keywords: Static typing, session types, non-uniform method availability, inheritance.

Current trends in hardware made available multi-core CPU systems to ordinary users, challenging researchers to devise new techniques to bring software into the multi-core world. However, shaping software for multi-cores is more envolving than simply balancing workload among cores. In a near future (in less than a decade) Intel prepares to manufacture and ship 80-core processors; programmers must perform a paradigm shift from sequential to concurrent programming and produce software adapted for multi-core platforms. In the last decade, proposals have been made to compile formal concurrent and functional languages, notably the pi-calculus, typed concurrent objects, and the lambda-calculus, into assembly languages. The last work goes a step further and presents a series of type-preserving compilation steps leading from System F to a typed assembly language. Nevertheless, all theses works are targeted at sequential architectures. This paper proposes a type-preserving translation from the pi-calculus into MIL, a multithreaded typed assembly language for multi-core/multi- processor architectures. We start from a simple asynchronous typed version of the pi-calculus and translate it into MIL code that is then linked to a run-time library (written in MIL) that provides support for implementation of the pi-calculus primitives (e.g., queuing messages and processes). In short, we implement a message-passing paradigm in a shared-memory architecture. /p>

Runtime Checking Java Code Using Congu

We analyse the relationship between object-oriented modelling and session-based, service-oriented modelling, starting from a typical UML Sequence Diagram and providing a program transformation into a service-oriented model. We also provide a similar transformation from session-based specifications into request-response specifications. All transformations are specified in \sscc---a process calculus for modelling and analysing service-oriented systems---and proved correct with respect to a suitable form of behavioural equivalence (full weak bisimilarity). Since the equivalence is proved to be compositional, results remain valid in arbitrary contexts.

We analyse the relationship between object-oriented modelling and session-based, service-oriented modelling, starting from a typical UML Sequence Diagram and providing a program transformation into a service-oriented model. We also provide a similar transformation from session-based specifications into request-response specifications. All transformations are specified in \sscc---a process calculus for modelling and analysing service-oriented systems---and proved correct with respect to a suitable form of behavioural equivalence (full weak bisimilarity). Since the equivalence is proved to be compositional, results remain valid in arbitrary contexts.

We define a small class-based object-oriented language in which the availability of methods depends on an object's abstract state: objects' interfaces are \emph{dynamic}. Each class has a \emph{session type} which provides a global specification of the availability of methods in each state. A key feature is that the abstract state of an object may depend on the result of a method whose return type is an enumeration. Static typing guarantees that methods are only called when they are available. We present both a type \emph{system}, in which the typing of a method specifies pre- and post-conditions for its object's state, and a typechecking \emph{algorithm}, which infers the pre- and post-conditions from the session type, and prove type safety results. Inheritance is included; a subtyping relation on session types, related to that found in previous literature, characterizes the relationship between method availability in a subclass and in its superclass. We illustrate the language and its type system with example based on a Java-style iterator and a hierarchy of classes for accessing files, and conclude by outlining several ways in which our theory can be extended towards more practical languages.
Keywords: Static typing, session types, non-uniform method availability, inheritance.

This report studies different definitions of bisimulation within the Stream-based Service-Centered Calculus (SSCC) and shows that both strong and weak ground bisimulation are non-input congruences.
Keywords: Process calculus, bisimulation, services.

The main goal of the ConGu project is the development of a framework to create property-driven algebraic specifications and test Java implementations against them. In this paper we present a brief overview of the framework's fundamental components -- specifications, modules, refinements -- and describe the ConGu tool both from the user's and from the architect's point of view. The tool allows users to test Java classes -- no source code needed, just bytecode -- against a module of specifications, and to discover runtime axiom violations. The tool generates intermediate classes equipped with contracts and wraps the original classes in classes that allow contract monitoring in a way that is transparent to the clients of the original classes. The tool generates JML assertions, but it could as well generate contracts in other assertion languages -- the ConGu modules that generate classes for monitoring are independent from those that generate contracts. We also report on the use of the ConGu tool in the context of an undergraduate programming course.

Congu is a tool that supports the checking of Java classes against property-driven algebraic specifications. This document presents the specification, languages, the tool usage, and its implementation, version 1.32. Chapter 1 describes the two specification languages: the language of abstract data types specifications, and that for defining refinement mappings between these specifications and Java classes. Chapter 2 explains how to install and use Congu tool. And finally, Chapter 3 presents the implementation details of the tool.

Session types support a type-theoretic formulation of structured patterns of communication, so that the communication behaviour of agents in a distributed system can be verified by static type checking. Applications include network protocols, business processes, and operating system services. In this paper we define a multithreaded functional language with session types, which unifies, simplifies and extends previous work. There are three main contributions. First: an operational semantics with buffered channels, instead of the synchronous communication of previous work. Second: session type manipulation by means of the standard structures of a linear type theory, rather than by means of new forms of typing judgement. Third: a notion of subtyping, including the standard subtyping relation for session types (imported into the functional setting) and a novel form of subtyping between standard and linear function types. Our new approach significantly simplifies session types in the functional setting, clarifies their essential features, and provides a secure foundation for language developments such as polymorphism and object-orientation, as well as further forms of static analysis including estimating the size of communication buffers.

We give a formal account of a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocol that services run when invoked (conversation). The calculus includes primitives for defining and invoking services, for isolating conversations between clients and servers, and for orchestrating services. The calculus is equipped with a reduction and a labeled transition semantics related by an equivalence result. To hint how the structuring mechanisms of the language can be exploited for static analysis we present a simple type system guaranteeing the compatibility between client and server protocols, an application of bisimilarity to prove equivalence among services, and we discuss deadlock-avoidance.

We give a formal account of a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocol that services run when invoked (conversation). The calculus includes primitives for defining and for invoking services, for isolating conversations between requesters and providers of services, and primitives for orchestrating services, that is, to make use of existent services as building blocks to accomplish complex tasks. The calculus is equipped with a reduction and a labeled transition semantics; an equivalence result relates the two. To give an hint on how the structuring mechanisms of the language can be exploited for static analysis we present a simple type system guaranteeing the compatibility between the protocols for service definition and for service invocation, and ensuring the sequentiality of each protocol.

Session primitives and types provide a flexible programming style for structural interaction, and are used to statically check a safe and consistent composition of protocols in communication-centric distributed software. They have been studied for the $\pi$-calculus, Ambients, CORBA interfaces, multi-threaded functional languages, Web Description Languages, and distributed and multi-threaded Java. This abstract reports the recent active discussions on the two fundamental theorems, Subject Reduction and Type Safety Theorems among the authors of session types. In the presence of higher-order session communication, session instantiation dynamically changes structures of sessions during execution, so that it becomes non-trivial to preserve typability. Unfortunately authors working on session types have recently realised that some of the previous systems fail to satisfy these basic theorems. Interestingly, the subtlety of type preservation is related to a treatment of communication channels in the rewriting rules of the $\pi$-calculus. After discussing the issues involved in higher-order session communication, this abstract also proposes a new session typing system which allows a more liberal higher-order session communication based on an idea of Gay and Hole. The new technical contributions of this abstract include: the formulation of the recursive types and proofs of the Subject Reduction and Type Safety Theorems of the original session typing system by Honda-Vasconcelos-Kubo in ESOP'98; and the introduction of a new session typing system and proofs of the two theorems for this system.

We seek for a small set of primitives that might serve as a basis for formalising and programming service oriented applications over global computers. As an outcome of this study we introduce here SCC, a process calculus that features explicit notions of service definition, service invocation and session handling. Our proposal has been influenced by Orc, a programming model for structured orchestration of services, but the SCC's session handling mechanism allows for the definition of structured interaction protocols, more complex than the basic request-response provided by Orc. We present syntax and operational semantics of SCC and a number of simple but nontrivial programming examples that demonstrate flexibility of the chosen set of primitives. A few encodings are also provided to relate our proposal with existing ones.

We present and evaluate an approach for the run-time conformance checking of Java classes against property-driven algebraic specifications. Our proposal consists in determining, at run-time, whether the classes subject to analysis behave as required by the specification. The key idea is to reduce the conformance checking problem to the runtime monitoring of contract-annotated classes, a process supported today by several runtime assertion-checking tools. Our approach comprises a rather conventional specification language, a simple language to map specifications into Java types, and a method to automatically generate monitorable classes from specifications, allowing for a simple, but effective, runtime monitoring of both the specified classes and their clients.

We present an assembly language targeted at shared memory multiprocessors, where CPU cores synchronize via locks, acquired with a traditional test and set lock instruction. We show programming examples taken from the literature on Operating Systems, and discuss a typing system that enforces a strict protocol on lock usage and that prevents race conditions.

Session primitives and types provide a flexible programming style for structural interaction, and are used to statically check the safe and consistent composition of protocols in communication-centric distributed software. Unfortunately authors working on session types have recently realised that some of the previously published systems fail to satisfy the basic theorems of Sub ject Reduction and Type Safety. This report discusses the issues involved in higher-order session communication, presents a formulation of the recursive types as well as proofs of the Subject Reduction and Type Safety Theorems of the original session typing system by Honda-Vasconcelos-Kubo in ESOP'98. It also proposes a new session typing system which allows a more liberal higher-order session communication based on an idea of Gay and Hole.

Design by contract (DBC) is among the most popular techniques that are taught in introductory programming courses aiming at helping students to learn how to construct correct and robust software. Although we recognize the important role played by formal design as supported by DBC techniques, we have experienced for several years the frustration of not being able to guide students in writing contracts, both that fully specify all the relevant properties, and are monitorable. The fact that students are left with very poor specifications leads them to perceive contracts as unnecessary and even irrelevant, discouraging the further application of DBC. We addressed these problems through the adoption of property-driven algebraic specifications for the description of the observable behavior of programs. Our approach comprises a tool-assisted refinement process that supports the run-time checking of implementations against specifications. In this paper we present the approach and report on our experience of using it.

This paper proposes the use of session types to extend with behavioural information the simple descriptions usually provided by software component interfaces. We show how session types allow not only high level specifications of complex interactions, but also the definition of powerful interoperability tests at the protocol level, namely compatibility and substitutability of components. We present a decidable proof system to verify these notions, which makes our approach of a pragmatic nature.

We present an approach for testing Java implementations of abstract data types (ADTs) against their specifications. The key idea is to reduce this problem to the run-time monitoring of contract annotated classes, which is supported today by several runtime assertion-checking tools. The approach comprises an ADT specification language that allows automatic generation of monitorable contracts and a refinement language that supports the specification of the details of object-oriented implementations of ADTs.

We present MiKO, a distributed process calculus obtained by instantiating Boudol's Generic Membrane Model with the TyCO language. In the membrane model, a network is composed of a collection of domains, each of which comprises an outer part, the membrane, and an inner part, the contents. The contents of the domain is its computational core. It interacts with the outside (the other domains in the network) using the membrane as intermediary. The membrane implements all protocols required to control the flow of information between the network and the contents of the domain. We provide an operational semantics and a type system for the calculus and prove subject reduction, together with some examples.

This paper presents a type system to control the migration of code between network nodes in a concurrent distributed framework, using the Dpi language. We express resource access policies as types and enforce policies via a type system. Types describe paths travelled by migrating code, enabling the control of history sensitive access to resources. Sites are logically organised in subnetworks that share the same security policies, statically specified by a network administrator. The type system guarantees that well-typed networks are exempt from security policies violations at runtime.

We describe the architecture and the implementation of the MIKADO software framework, that we call IMC (Implementing Mobile Calculi and show how it can be used. The framework aims at providing the programmer with primitives to design and implement run-time systems for distributed process calculi. The document describes the four main components of abstract machines for mobile calculi (node topology, naming and binding, communication protocols and mobility) that have been implemented as Java packages. The document ends with the description of three implementation experiments that use IMC: the re-implementation of KLAVA, the run time support for KLAIM, the implementation of a runtime system for the Distributed Pi-Calculus and the development of an instance calculus of Boudol s membrane model.

We analyse machines that implement the call-by-value reduction strategy of the lambda-calculus, namely, two environment machines---CAM and SECD---and two encodings into the pi-calculus---due to Milner and Vasconcelos. To establish the correspondences between the various machines, we setup a notion of reduction machine and two notions of correspondences: operational---in which a reduction step in the source machine is mimicked by a sequence of steps in the target machine, modulo equivalence---and convergent---where only reduction to normal form is simulated. We show that there are operational correspondences from the lambda-calculus into CAM, and from CAM and from SECD into the pi-calculus. Plotkin completes the picture by showing that there is a convergent correspondence from the lambda-calculus into SECD.

We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static typechecking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus typechecking can verify both correctness of individual messages and correctness of sequences of transitions. Previously, session types have mainly been studied in the context of the $\pi$-calculus; instead, our formulation is based on a multi-threaded functional language with side-effecting input/output operations. Our typing judgements statically describe dynamic changes in the types of channels, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and type checking system of our language, and prove subject reduction and runtime type safety theorems.

Session Types for Functional Multithreading

We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static typechecking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus typechecking can verify both correctness of individual messages and correctness of sequences of transitions. Previously session types have mainly been studied in the context of the -calculus; instead, our formulation is based on a multi-threaded functional language with side-effecting input/ output operations. Our typing judgements statically describe dynamic changes in the types of channels, our channel types statically track aliasing, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and typing rules of our language, and prove subject reduction and runtime type safety theorems.
Keywords: Session types, static typechecking, concurrent programming, specification of communication protocols.

We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static typechecking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus typechecking can verify both correctness of individual messages and correctness of sequences of transitions. Previously session types have mainly been studied in the context of the -calculus; instead, our formulation is based on a multi-threaded functional language with side-e ecting input/ output operations. Our typing judgements statically describe dynamic changes in the types of channels, our channel types statically track aliasing, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and typing rules of our language, and prove subject reduction and runtime type safety theorems.

This paper presents a type system to control the migration of code between nodes in a concurrent distributed framework, using Dpi. We express resource policies with types and enforce them via a type system. Sites are organised hierarchically in subnetworks that share the same security policies, statically specified by a network administrator. The type system guarantees that, at runtime, there are no security policies violations.

This paper describes a proposal for typing the behavior of objects in component models. Most component models, CORBA in particular, do not offer any support for expressing behavior al properties of objects beyond the ``static'' information provided by IDLs. We build on the works by Honda et al. and Gay and Hole to show how session types can be effectively used for describing protocols, extending the information currently provided by object interfaces. We show how session types not only allow high level specifications of complex object interactions, but also allow the definition of powerful interoperability tests at the protocol level, namely compatibility and substitutability of objects

We describe a reference implementation of a multi-threaded run-time system for a core programming language based on a process calculus. The core language features processes running in parallel and communicating through asynchronous messages as the fundamental abstractions. The programming style is fully declarative, focusing on the interaction patterns between processes. The parallelism, implicit in the syntax of the programs, is effectively extracted by the language compiler and explored by the run-time system.

We define a lexically scoped, asynchronous and distributed pi-calculus with local communication and process migration. This calculus adopts the network-awareness principle for distributed programming and follows a simples model of distribution for mobile calculi: a lexical scoping discipline combines static scoping with dynamic linking, associating channels to a fixed site throughout computation. Furthermore, it provides for both remote invocation and process migration. A simple equivalence law captures the essence of the model: a process behaviour depends on the names it uses, not where it runs.

We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static typechecking. A session type, associated with a communication channel, specifies not only the data types of individual messages, but also the state transitions of a protocol and hence the allowable sequences of messages. Although session types are well understood in the context of the pi-calculus, our formulation is based on lambda-calculus with side-effecting input/output operations and is different in significant ways. Our typing judgements statically describe dynamic changes in the types of channels, our channel types statically track aliasing, and our function types not only specify argument and result types but also describe changes in channel types. After formalising the syntax, semantics and typing rules of our language, and proving a subject reduction theorem, we outline some possibilities for extending this work to a concurrent object-oriented language.

This paper describes a proposal for typing the behavior of objects in component models. Most component models, CORBA in particular, do not offer any support for expressing behavior al properties of objects beyond the ``static'' information provided by IDLs. We build on the works by Honda et al. and Gay and Hole to show how session types can be effectively used for describing protocols, extending the information currently provided by object interfaces. We show how session types not only allow high level specifications of complex object interactions, but also allow the definition of powerful interoperability tests at the protocol level, namely compatibility and substitutability of objects.

We describe a linear channel inference system for the TyCO programming language, where channel usage is tracked through method invocations as well as procedure calls. We then apply linear channel information to optimize code generation for a multithreaded runtime system. The impact in terms of speed and space is analyzed.

We present the approach to teach object-oriented concepts that we have adopted almost three years ago. Our integrated effort spreads over three one-semester courses, incorporated in a four year long undergraduate course, and is based on a objects-first approach coupled with contract-guided system development. Our aim is that students learn the fundamental skills to the construction of correct, robust, reuseable and extensible software systems. Some preliminary conclusions are presented.

We define the syntax, the operational semantics, and a type system for lsdpi, an asynchronous and distributed pi-calculus with local communication and process migration. The calculus follows a simple model of distribution for mobile calculi, with a lexical scoping mechanism that provides for both remote communication and process migration, and makes explicit migration primitives superfluous.

We present an extension to the TyCO type system that is able to identify linear channels. We prove some technical results (e.g. type preservation w.r.t. reduction) and present an algorithm for inferring channels usage from process expressions. Our major contribution is the inference of linear information in a calculus with recursive equations rather than replication.

This paper presents a multithreading abstract machine for the TyCO process calculus. We argue that process calculi provide a powerful framework to reason about fine-grained parallel computation. They allow for the construction of formally verifiable system on which to base high-level programming idioms, combined with efficient compilation schemes into multithreaded architectures.

TyCO stands for ``TYped Concurrent Objects''. Not that the language includes any form of primitive objects. Instead, a few basic constructors provide for a form of Object-Based Programming (that is, objects but no inheritance). The language is quite simple. The basic syntax reduces to half-a-dozen constructors. To help in writing common programming patterns, a few derived constructors are available. This report introduces TyCO by example, rather than explaining the language first and giving examples second.

This is the third report on TyCO, a (still) experimental strongly and implicitly typed concurrent object based programming language based on a predicative polymorphic calculus of objects, featuring asynchronous messages, objects, and procedures, together with a predicative polymorphic typing assignment system, assigning monomorphic types to variables and polymorphic types to procedures.

2000

We propose a programming model for distributed concurrent systems with mobile objects in the context of a process calculus. Code mobility is induced by lexical scoping on names. Objects and messages migrate towards the site where their prefixes are lexically bound. Class definitions, on the other hand, are downloaded from the site where they are defined, and are instantiated locally upon arrival. We provide several programming examples to demonstrate the expressiveness of the model. Finally, based on this model we describe an architecture for a run-time system supporting concurrent, distributed computations and code mobility.

Concurrent objects may offer services non-uniformly, constraining the acceptance of messages on the states of objects. We advocate a looser view of communication errors. Safe programmes must guarantee that every message has a chance of being received if it requests a method that may become enabled at some point in the future. We formalise non-uniform concurrent objects in TyCO, a name-passing object calculus, and ensure program safety via a type system. Types are terms of a process algebra that describes dynamic aspects of the behaviour of objects.

We present an encoding of the call-by-value lambda-calculus into the pi-calculus, alternative to the well-known Milner's encodings. We show that our encoding is barbed congruent (under typed contexts) to Milner's ``light'' encoding, and that it takes two pi-steps to mimic a beta-reduction for normalizing terms. We describe a translation of Plotkin's SECD machine into the pi-calculus, and show that there is an operational correspondence between a SECD machine and its encoding. Equipped with a notion of state-based machine and two kinds of correspondences between them, we compare the encodings of the call-by-value lambda-calculus and the SECD machine into the pi-calculus.

We propose a new type discipline for the pi-calculus in which secure information flow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by subtyping. A behavioral notion of types capturing causality of actions plays an essential role for ensuring safe information flow in diverse interactive behaviours, making the calculus powerful enough to embed known calculi for type-based security. The paper introduces the core part of the calculus, presents its basic syntactic properties, and illustrates its use as a tool for programming language analysis by a sound embedding of a secure multi-threaded imperative calculus of Volpano and Smith. The embedding leads to a practically meaningful extension of their original type discipline.

We propose a new type discipline for the pi-calculus in which secure information flow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by subtyping. A behavioral notion of types capturing causality of actions plays an essential role for ensuring safe information flow in diverse interactive behaviours, making the calculus powerful enough to embed known calculi for type-based security. The paper introduces the core part of the calculus, presents its basic syntactic properties, and illustrates its use as a tool for programming language analysis by a sound embedding of a secure multi-threaded imperative calculus of Volpano and Smith. The embedding leads to a practically meaningful extension of their original type discipline. Other fundamental technical elements, culminating in the behavioural non-interference result, are also sketched.

We propose a simple formal model of distribution for mobile objects in the context of the TyCO process calculus. Code mobility is induced by lexical scoping on names and template process definitions. Objects and messages migrate towards the site where their prefix names are lexically bound. Template process definitions, on the other hand, are downloaded from the site where they are defined, and are instantiated locally upon arrival. Based on this model we describe the run-time support for distribution and code mobility implemented in DiTyCO, an extension of the TyCO programming language.

A Virtual Machine for the TyCO Process Calculus

Despite extensive theoretical work on process-calculi, virtual machine specifications and implementations of actual computational models are still scarce. This paper presents a virtual machine for a strongly typed, polymorphic, concurrent, object-oriented programming language based on the TyCO process calculus. The system runs byte-code files, assembled from an intermediate assembly language representation, which is in turn generated by a compiler. Code optimizations are provided by the compiler coupled with a type-inference system. The design and implementation of the virtual machine focuses on performance, compactness, and architecture independence with a view to mobile computing. The assembly code emphasizes readability and efficient byte code generation. The byte code has a simple layout and is a compromise between size and performance. We present some performance results and compare them to other languages such as Pict, Oz, and JoCaml.

We present an undecidability proof of the notion of communication errors in the polyadic pi-calculus. The demonstration follows a general pattern of undecidability proofs - reducing a well-known undecidable problem to the problem in question. We make use of an encoding of the lambda-calculus into the pi-calculus to show that the decidability of communication errors would solve the problem of deciding whether a lambda term has a normal form.

Based on a name-passing calculus and on its typing system we show how to build several language constructors towards strongly-typed concurrent programming languages. In particular, we introduce a notion of datatype declaration, and show how to create values of a datatype and how to take such values apart. Further expressions include a form of abstraction and of application. Expressions evaluate to names and can replace any (non-binding) name in the calculus, thus achieving a clean incorporation of expressions in a name-passing calculus. A systematic translation of the derived constructors into the basic calculus provides for the semantics and for typing rules for the new constructors.

We propose a simple model of distribution for mobile processes, independent of the underlying calculus. Conventional processes compute within sites; inter-site computation is achieved by message sending and object migration, both obeying a lexical scope. We focus on the semantics of networks, on programming practice, and on physical realisation with current technology.

We propose an algebra of object types that characterises the semantics of concurrent objects in a process calculus setting where the communication is asynchronous. The types are non-uniform, and provide an internal (and synchronous) view of the objects th at inhabit them. These ideas, along with the algebraic laws, are based on a notion of bisimulation that is unlike other notions in the literature.

We introduce basic language constructs and a type discipline as a foundation of structured communication-based concurrent programming. The constructs, which are easily translatable into the summation-less asynchronous pi-calculus, allow programmers to organise programs as a combination of multiple flows of (possibly unbounded) reciprocal interactions in a simple and elegant way, subsuming the preceding communication primitives such as method invocation and rendez-vous. The resulting syntactic structure is exploited by a type discipline à la ML, which offers a high-level type abstraction of interactive behaviours of programs as well as guaranteeing the compatibility of interaction patterns between processes in a well-typed program. After presenting the formal semantics, the use of language constructs is illustrated through examples, and the basic syntactic results of the type discipline are established. Implementation concerns are also addressed.

This is the second report on TyCO, a (still) experimental strongly and implicitly typed concurrent object oriented programming language based on a predicative polymorphic calculus of objects, featuring asynchronous messages, objects, and process declarations, together with a predicative polymorphic type system.

Despite extensive theoretical work on process-calculi, abstract machine specifications and implementations of actual computational models are still scarce. Moreover, a general framework for compiling languages based on these calculi is still elusive. We propose a core assembly language onto which process-calculi based languages may be compiled and present a specification for a self-contained abstract machine that runs this assembly code. We also include compilation examples of features of well known calculi and discuss possible optimizations. Finally, we report preliminary performance results obtained with an implementation of the abstract machine coupled with an experimental language based on the TyCO-calculus.

We present an abstract machine specification for TyCO (Typed Concurrent Objects), a name-passing calculus that aims at capturing fundamental concepts present in Concurrent Object-Oriented Languages. TyCO has built-in labeled messages and ephemeral object s that communicate asynchronously. Persistent objects are supported through instantiation of recursive classes. Concurrency is pervasive and synchronous communication can be implemented by passing continuations in messages. Strong, static typing is provided by a type inference algorithm that supports a form of predicative polymorphism. This paper describes the abstract machine framework in detail, including how it evolves from TyCO and some important properties it can be shown to possess.

We present an abstract machine specification for TyCO (Typed Concurrent Objects), a name-passing calculus that aims at capturing fundamental concepts present in Concurrent Object-Oriented Languages. TyCO has built-in labeled messages and ephemeral objects that communicate asynchronously. Persistent objects are supported through instantiation of recursive classes. Concurrency is pervasive and synchronous communication can be implemented by passing continuations in messages. Strong, static typing is provided by a type inference algorithm that supports a form of predicative polymorphism.
This paper presents the formal framework of the TyCO abstract machine.

We present a new type system for TyCO, a name-passing calculus of concurrent objects. The system captures dynamic aspects of objects' behaviours, namely non-uniform service availability of objects. The notion of processes without errors is loosened, demandind only weak fairness in the treatment of messages.

We present an operational semantics and a typing assignment system for the concurrent object-oriented specification language Gnome, based on a name-passing asynchronous calculus of concurrent objects, TyCO. The operational semantics is given by a map encoding Gnome classes in TyCO agents, and thus, objects (instances of classes) in processes (instances of agents). We propose a general approach to implement synchronous communication in an asynchronous process calculus, using a commit-abort protocol, achieving by this means the synchronization of all objects involved on a transaction. We treat objects with internal animation, their dynamic creation and deletion. Furthermore, the method generates a (decidable) typing assignment system that ensures lack of runtime errors for typable programs. The type of an agent certificates the communicating protocol of the corresponding class.

We propose a computation model based on the separation between truth and action. The state of an agent is considered to consist of two components: the task, representing actions to be performed, and the database, representing certain truths. The task specifies a composition (parallel, sequential, choice, synchronous) of elementary actions: queries and commands. Queries may only be executed when certain truths are entailed by the database. Commands always execute and as an effect may change the database. We thus have the osmosis metaphor: the task and database are separated as if by a membrane through which information flows in both directions causing the system to evolve. Truth may enable actions (queries) to be accomplished, and actions (commands) may change what is true. Commands are assumed to have a deterministic nature. We discuss the fundamental semantic properties needed for accommodating this basic model, and consider extensions to accomodate named tasks and their refinement rules, variables in tasks, and systems of named agents with separate rules and databases.

The present report presents an operational semantics and a typing system for ABCL/1 programs, based on a name-passing calculus. The particular calculus we use, TyCO, features asynchronous labelled message passing, explicit objects composed of labelled methods, and operators to compose objects and messages concurrently, and to generate new names. The calculus is only implicitly typed in that no type information is presented in programs, but else inferred through a typing assignment system. The operational semantics is obtained by a systematic translation of the constructors present in the ABCL/1 language into TyCO processes. The type assignment system is derived from this encoding and from TyCO type inference rules. The encoding provides a very fine grain semantics that makes explicit the order of evaluation in methods, and highlights the most complex features present in ABCL/1, namely wait-for forms and express-messages. The typing system provides a means to statically separate ``safe programs'' from programs that may run into errors at runtime, and in particular avoids testing the type of arguments in methods. There is an algorithm capable of extracting the most general type of an ABCL/1 program, or to detect its inexistence.

We study the problem of unifying infinite trees with variables subject to constraints on the trees they may be substituted for. The constraints are given by mappings from variables to trees, called kindings. In particular, we show that if a set of equations over a given kinding is unifiable, it has a most general unifier using only a subset of the variables in the set of equations and in the kinding. We present an algorithm to extract the most general unifier of a regular (having a finite number of subtrees) and unifiable set of equations over a given kinding. The results extend those of Huet on unification of regular trees, and those of Ohori on unification of kinded finite trees.

I propose an untyped name-passing calculus and a series of decidable type systems assigning types to names in terms. The calculus, designed according to the modern trends in name-passing calculi, is intended to capture the basic concepts of concurrent objects. The type systems, developed along the lines of those for lambda-calculi, provide for partial-specification in the form of communication protocols for programs, and for partial-correctness wherein typable terms are assured not to run into errors at execution time.
Terms are built from names and labels by means of five constructors, the innovations being guarded labelled-sums describing objects composed of labelled methods and asynchronous labelled messages selecting a method in the target object. The remaining constructors are fairly standard in name-passing calculi and comprise concurrent composition, local name creation (or scope restriction), and replication.
The type systems assign types to names, and typings (that is, sets of name-type pairs) to terms. Simple types are built from type-variables by means of a single record constructor that uses the labels in the syntax of the calculus. To realize typing terms containing circular name-structures, a recursive type constructor is introduced, recursive types being viewed as regular (that is, having finitely many subtrees) infinite trees. The main properties of these type systems are subject-reduction (implying that typable terms do not encounter errors at execution time), decidability of typing assignment, and computability of typing inference. Nonetheless, no notion of typing subsumption, and hence of principal typings, seems to be possible in these systems. I use constraints on the types that may replace a given type-variable, and study the problem of unifying infinite trees with variables subject to constraints.
From a pragmatic point of view, the calculus provides the building blocks necessary to describe the formal operational semantics of concurrent object-oriented programming languages; more complex notions of objects are easily encoded into the basic calculus. Simultaneously, the type systems developed can be used to derive type systems for high-level programming languages. From a theoretical point of view, this work brings into the name-passing paradigm (not restricted to the calculus presented, but encompassing the pi-calculus and the nu-calculus) the notions of types and type assignment, thus opening the possibility to explore, in the setting of name-passing calculi, the wide body of results on type systems for lambda-calculi.

We present a formulation of the polyadic pi-calculus featuring a syntactic category for agents, together with a typing system assigning polymorphic types to agents. The new presentation introduces an operator to express recursion, and an ML-style let-constructor allowing to associate an agent to an agent-variable, and use the latter several times in a program. The essence of the monomorphic type system is the assignment of types to names, and multiple name-type pairs to programs. The polymorphic type system incorporates a form of abstraction over types, and inference rules allowing to introduce and eliminate the abstraction operator. The extended system preserves most of the syntactic properties of the monomorphic system, including subject-reduction and computability of principal typings.
We present an algorithm to extract the principal typing of a process, and prove it correct with respect to the typing system. We also study, in the context of pi-calculus, some well-known properties of the let-constructor.

Based on a name-passing calculus and on its typing system the paper shows how to build several language constructors towards a strongly-typed object-oriented concurrent programming language. The basic calculus incorporates the notions of asynchronous labelled messages, concurrent objects composed of labelled methods, and a form of abstraction on processes allowing in particular to declare polymorphic classes. We introduce a notion of values as name-expressions, and show how to create subclasses of existing classes. A systematic translation of the derived constructors into the basic calculus provides for semantics and for typing rules for the new constructors.

We introduce a name-passing calculus featuring objects as guarded labelled-sums, each summand representing a method, and asynchronous labelled messages selecting a branch in the sum. A decidable type assignment system allows to statically verify whether all possible communications in a given program are secure, in the precise sense that no object will ever receive a message for which it does not have an appropriate method. Then we present a recursive type system based on that of Cardone and Coppo for the lambda-calculus, and of Vasconcelos and Honda for the polyadic pi-calculus. The new system extends the class of typable terms while preserving basic syntactical properties of the simple type system, including subject-reduction and existence and computability of principal typings.

The present paper introduces an implicitly typed object calculus intended to capture intrinsic aspects of concurrent objects communicating via asynchronous message passing, together with a typing system assigning typings to terms in the calculus. Types meant to describe the kind of messages an object may receive are assigned to the free names in a program, resulting in a scenario where a program is assigned multiple name-type pairs, constituting a typing for the process. Programs that comply to the typing discipline are shown not to suffer from runtime errors. Furthermore the calculus possesses a notion of principal typings, from which all typings that make a program well-typed can be extracted. We present an efficient algorithm to extract the principal typing of a process.

The present paper introduces a typing system for a version of Milner's polyadic pi-calculus, and a typing inference algorithm linear on the size of the input. The central concept underlying the typing system is the notion of type assignment, where each free name in a term is assigned a type, the term itself being given multiple name-type pairs. This observation leads to a clean typing system for Milner's sorting, and induces an efficient algorithm to infer the typing of a term. The typing system enjoys a subject-reduction property and possesses a notion of principal typing scheme. The algorithm to reconstruct the principal typing scheme of a process, or to detect its inexistence, is proved correct with respect to the typing system.

We study a typing assignment system for the higher-order pi-calculus. The system proposed is a straightforward extension of the typing system for the polyadic pi-calculus proposed by Kohei Honda and the author, by introducing a new type constructor for agents (i.e., processes abstracted on some sequence of names and variables.) We also present an efficient typing reconstruction algorithm to extract the most general typing of an agent or to detect its inexistence, and prove its correctness with respect to the typing system. Finally we show that well-sorted agents are typable, and that typable agents are well-sorted, thus establishing the correspondence between Davide Sangiorgi's sorting system and the typing assignment system.

The present paper introduces an untyped calculus of intended objects to capture intrinsic aspects of concurrent objects communicating via asynchronous message passing, together with a typing system assigning typings to terms in the calculus. Types meant to describe the kind of messages an object may receive are assigned to the free names in a program, resulting in a scenario where a program is assigned multiple name-type pairs. Then, a ML-like let declaration is introduced together with an extension of the monomorphic typing assignment system, which allows to declare a term of a polymorphic type and use it multiple times with different types, instances of the type of the declared term. The system enjoys desirable properties, such as subject-reduction which implies that programs that comply to the typing discipline do not suffer from runtime errors, as well as the existence and computability of principal types. Furthermore, we present an efficient algorithm to extract the principal typing of a term.

This is the first report on TyCO, an experimental strongly typed concurrent object oriented programming language. It is an interactive language based on the Calculus of Objects featuring asynchronous messages, objects, concurrency and process declaration in an implicitly typed simple language, together with a powerful predicative polymorphic typing assignment system assigning monomorphic types to free names in programs and polymorphic types to process declarations. The grammar of the language and its static semantics are given in the style of Standard ML; dynamic semantic are not considered here.

The theory of traces (free partial commutative monoids) is used to describe the behavior of systems of concurrent objects. A composition operation on systems and a synchronization operation on behaviors are presented: they allow to derive the behavior of complex systems from the behavior of its components.
To address fundamental issues of concurrent semantics for objects in general, we concentrate on a simple model where objects communicate via asynchronous message passing and are only capable of sending messages, creating more objects and changing the way they react to incoming messages.
The semantics is built from two simple concepts: a set of events representing the reception of messages by objects, and a binary symmetric and irreflexive relation on events - independence - representing permissible concurrency. Causality, the dual notion of concurrency, is expressed by the dependence relation - the complement of independence. Executions of systems are described by a traces: labeled acyclic graphs where nodes are labeled with events and the only edges are between different nodes labeled with dependent events. The behavior of a system is the set of traces representing all possible executions.
We achieve a simple and intuitive description of the behavior of concurrent objects where both causality and concurrency are explicit. When compared to other semantics for concurrent objects, trace semantics yields a more abstract description, in the sense that more similarly behaving computations are identified.

The theory of traces is used to describe the behavior of actor systems. The semantics is built from two simple concepts: a set of events representing the reception of messages by objects, and a binary symmetric and irreflexive relation on events - independence - representing permissible concurrency. Causality, the dual notion of concurrency, is expressed by the dependence relation - the complement of independence. A particular execution of a system is described by a trace: a labeled acyclic graph where nodes are labeled with events and the only edges are between nodes labeled with dependent events. The behavior of a system is viewed as the set of traces representing all possible executions. Finally, a composition operation on systems and a synchronization operation on behaviors are presented: they allow to derive the behavior of complex systems from the behavior of its components.