This CAREER award supports an investigation into the use of type theory and operational semantics in the design and implementation of programming languages. Type theory has proved to be an important organizing principle in programming language design. This is well exemplified by the use of type theory in the design of modularity and abstraction constructs. This investigation seeks to consolidate advances in type theory into the design of the ML2000 programming language. Type theory has proved important for the implementation of programming languages. Conventional syntax-directed compilation methods are generalized to type-directed compilation, allowing type information to be exploited during compilation. Sophisticated type systems such as those derived from the Girard- Reynolds polymorphic lambda-calculus suggest new implementation strategies based on passing type information at link- and run- time. This research investigates the use of type-based compilation techniques. Operational semantics provides a suitable framework for addressing issues of compiler correctness and proving properties of programs. Typed programming languages such as Standard ML provide a rich setting in which to discuss high-level programming techniques such as data abstraction, modularity, and separate compilation. Types are essential for reasoning about programs. A procedure can in general be deemed to have certain input/output properties only under the assumption that its arguments have suitable types. Operational semantics is a useful pedagogical tool for teaching undergraduate programming, both as an explanatory device and as the basis for proving properties of programs and languages. Important advantages are expected through the interplay between research and education.
