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 rst 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. How