On Bounded Polymorphic Session Type System

Wide application of network technology and Web service technology promotes the rapid development of concurrent distributed computing, whose main characteristics are concurrency, distribution, real time and so on. Because of these complex features, concurrent distributed systems are facing the challenges of communication safety. In order to explore the behavior of concurrent distributed system and ensure communication safety, lots of distributed computing models have been put forward, which are based on inter-process communication and reflect concurrency, such as models of CSP, CCS, Pi-calculus and so on. Session type theory is a new theoretical model referring to concurrent computing, which inherits the basic syntax and the ideology of using reduction to express the communicating behavior between processes from Pi-calculus, and leads into type theory. Session type theories not only can construct and reason about inter-process actions but also capture the protocol discipline between communicating processes better. Typing rules of session type theories can be translated into a practical type detection algorithm, so it is an effective formal method of reasoning about communication behavior.Basic theory and framework of session type system are firstly introduced in this thesis, and then we improve the message delivery mechanism on the basis of the original bounded polymorphic session type system. At last, we use examples to elaborate significance of this thesis. The main contribution in this thesis is as follows:(1) Session type theory is proposed based on Pi-calculus, so it inherits the merits of Pi-calculus, such as concise syntax, reduction and so on. Previous session type system unified variables and channel as name, this can not reflect the process of data and channel delivery well. Therefore, by conjunction with previous studies, we put forward a new bounded polymorphic session type system with delegation, which distinguishes data transmission from channel delivery and defines their syntax, semantics and typing rules separately.(2) In order to reflect the session type change of channel during delivery much better, we improves the environment of the past session type systems by adding channel environment C, so the judgement form changes from△;Γ├P into△;Γ├P?C. According to this point, new typing rules can trace for the order of channel using well, reflect the change of channel type clearly and get a more direct expression of various message-passing processes.(3)Safety is a basic property of session type system. The so called safety refers that a well-formed process can reduce any sequence of steps and error does not occur. This paper proves the completeness of this system from two aspects:subject reduction and type safety. After the proof, we exemplify the process of message delivery and reflect the changes of channel types in the process of messaging.