Type Systems for Guaranteeing Resource Bounds of Component Software

Since the early days of the development of programming languages, people have been developing various methods to reduce the runtime errors of software programs. These methods range from static analysis, testing to runtime monitoring. The first method is usually preferable if possible since it allows us to detect certain errors of programs before their execution. Type systems are a lightweight method of static analysis and they will be the main interest of the thesis. Type systems are a syntactic method for proving that certain kinds of programming errors cannot occur. Traditionally, they are used to guarantee that the parameters passed to a function are always of the right data type. Recently, many complex type systems are incorporated into mainstream programming languages and people are actively exploring their other capabilities. We study type systems for preventing errors caused by a lack of resources. Recently, component software facilitates building large, evolving software systems from a collection of standard reusable components, which can be developed independently. However, component software has a latent problem with resources. Due to the independent development and reuse of components, during the execution of a component program, several instances of the same component may be alive at the same time. For some components, creating a number of coexistent instances more than a certain number is not allowed or exceptions will occur. Examples are components that use special resources such as serial communication ports or database connections. Preventing this class of exceptions by static type systems is the subject study of this thesis. This thesis develops static type systems for abstract component languages so that well-typed programs will not use more resources than a certain bound. Putting it differently, through the types we know statically the maximum resources that a program needs so that if a system has enough such resources, executing the program on the system will never cause out-of-resource exceptions