A type system for a higher-order language

Abstract

In any computing device, resources a.re limited, and their demand is greater than their availability. Therefore, we must reuse resources for different purposes. However, this usually gets in the way of programming, especially since a resource can only be used by one process at a time. Further risks arise when we allow higher-order code to be transferred between concurrent processes. Even though the type system for the basic pi-calculus is sound, it discards a lot of well-behaved processes. In this FYP I designed a type system to statically reason about an extension of the pi-calculus in which processes can be sent over channels, and channels can be re-used whenever it is safe to do so.