Today's software systems are becoming more and more complicated due to the need of integrating various computation resources available in the Internet. A key to control the complexity and to enhance the reliability of such a system is to develop a high-level programming language that can directly represent various resources and automatically detect potential inconsistencies among the components in a system.
  Based on this general observation, our research aims at establishing both firm theoretical basis and implementation techniques for a flexible and reliable programming language. One direction toward this goal is to establish logical foundations for compilation, such as a proof-theory that accounts for the entire process of compilation including A-normalization and code generation as a series of proof transformation. We are also developing a new practical ML-style programming language, SML#, that embodies some of our recent results such as record polymorphism, and seamless interoperability with existing practical programming languages and relational databases.