This project conducts research on the design, definition, and implementation of programming languages, with emphasis on type structure and on bridging the gap between functional and imperative programming. In studying how to implement the programming language Forsythe, it investigates better methods of type checking for intersection types. Considerable improvement is expected from using a top-down rather than the present bottom- up algorithm. A more flexible approach to the implementation of procedures is also investigated, where a portion of the procedure body is compiled into closed code while the rest of the body is compiled into inline code at each call site. This is expected to substantially alleviate the overhead associated with call by name. The research seeks to unify two of the intractable dichotomies that complicate and divide the study of programming languages. The goal is to unify semantics based on domains, which permits partial and infinite computations, with semantics based on partial equivalence relations and intuitionistic type theory, which is limited to always-terminating computations. Also investigated is the unification of earlier work on the syntactic control of interference in Algol-like languages with the more recent development of low-level functional languages based on linear logic. In particular, this research would connect the concept of passive types with the modal operators of linear logic.
