Strong economic arguments favor the construction of software systems from off-the-shelf components. To ensure reliability and maintainabilty, it is vital that components come with precise, verifiable, and enforceable descriptions of their behavior. Rich modular programming mechanisms such as are found in the ML family of languages go a long way toward supporting component software. The key to their success is a strong type-theoretic foundation that provides clear assurances of the behavior of well-typed components. Harper will review the progress that has been made on the design and application of ML-like module systems. He will also discuss some recent ideas for enriching the specifications to admit description and enforcement of detailed protocols for component interaction.

Robert Harper is an Associate Professor of Computer Science at Carnegie Mellon University. His primary research interest is in the application of type theory to the design and implementation of programming languages. He is best known for his work on the design, semantics, and implementation of Standard ML and for his work on logical frameworks for describing and implementing formal logical systems.