| More than being just a tool for expressing algorithms, a well-designed programming language allows the user to express her ideas efficiently. The design choices, however, affect the efficiency of the algorithms written in the languages. It is therefore important to understand how such choices affect the expressibility of programming languages. The dissertation approaches this problem from two different angles.; First, the dissertation presents the first resource-independent characterization of the functions computable in logarithmic space ( LF). The characterization is done in the form of a function algebra BC-3 that is sound and complete for LF. BC-3 provides insights into restricting recursion which might be useful to provide compiletime guarantees on resource bounds. Furthermore, by comparison with work by Bellantoni and Cook, it highlights linearity as a potential distinction between the functions computable in logarithmic space (LF) and polynomial time (PF).; Secondly, the dissertation formalizes how successful type inference fundamentally depends on the amnesia of the type system: the fact that the type system forgets information about the program. Intersection type systems without idempotency provide an exact analysis where all information is retained. The dissertation shows that in such intersection type systems, normalization is equivalent to type inference in every single case. Thus, time bounds on type inference and normalization are identical, and doing compile-time type inference is useless.; The latter part reveals that expansion variables proposed for type inference are closely related to the boxes already known from the linear logic technology of proofnets. This hitherto unknown connection between the two technologies suggests fruitful contributions between the two fields. Moreover, the dissertation extends and formalizes a previously known connection between intersection types and proofnets. |
