Type discipline for message-passing components in distributed systems

Component based software engineering (CBSE) is a method- ology that aims to design and build software systems by assembling together reusable and loosely coupled compo- nents. Applying CBSE in a distributed setting is appealing but challenging: distributed applications require different remote components to interact following a well-defined protocol. This thesis addresses a model for message passing component-based systems where components are assembled together with the protocol itself. Components can there- fore be independent from the protocol, and can react to messages in a flexible way. This thesis studies how types can capture component behaviour and can enable checking the compatibility with a protocol. In particular, this thesis proposes two type languages for reactive components: the first language excludes choice terms, whereas the second one includes them. We show the correspondence of component and type behaviours, which entails a progress property for components.