This award is under the International Postdoctoral Fellows Program, which enables U.S. scientists and engineers to conduct three to twelve months of research at foreign centers of proven excellence. The program's awards provide opportunities for joint research, and the use of unique or complementary facilities, expertise and experimental conditions abroad. This award will support a twelve-month postdoctoral research visit by Dr. Penny Anderson to work with Dr Gilles Kahn, at INRIA Sophia-Antipolis, France. This research will explore how the wealth of theoretical work in formal logic, proof theory, logical frameworks, and related topics can be used to improve programming practice. Dr. Anderson will investigate the use of higher- order abstract syntax and related techniques in systems based on formal deduction that have efficient and well-designed user interfaces. Effective user interfaces are essential for most of the activities one might wish to undertake with the support of automated deductive systems: theorem proving, language prototyping, semantic analysis, program development, etc. These tasks require the management of large amounts of detail, and for even medium-sized problems they become infeasible without extensive support for presenting information to the user. In order to carry out experiments with deductive systems that are needed to bring theoretical work to practical application, one needs user interface tools that are general in the same sense that logical frameworks are. The use of higher- order encoding techniques has the potential to simplify the task of tailoring user interface tools to particular formal deduction systems. The purpose of this research is to bring together research in the application of logical frameworks with research in user interfaces to deduction-based systems. This should result in better understanding of implementation techniques and useful refinements of the underlying framework; the use of these encodings should clarify the semantic basis of the interaction with the user.
