US-France (INRIA) Cooperative Research: Type Theory and Interactive Development of Proofs and Programs

点击翻译按钮获取中文摘要

This award will support a group research effort in computer science to be carried out by researchers based at the University of Pennsylvania, Stanford University and Cornell University in collaboration with the French National Institute for Information Science and Automation (INRIA) and the Ecole Normale Superieure, Paris. The U.S. group will be led by Dr. Carl Gunter and Dr. Val Breazu-Tannen, University of Pennsylvania. On the French side the project will be led by Dr. Thierry Coquand, INRIA Rocquencourt. The three year program of joint visits and workshops will focus on the theory and applications of type systems. This group of U.S. researchers and their French counterparts have produced important results at the interface between the theory of programming, logic and algebra. Researchers are presently witnessing a convergence between logic, mathematics and computer science, in which, for example, deep connections between types, proofs and programs are being discovered. However, much remains to be done and discoveries of further connections and parallels are anticipated. As in any other rapidly advancing field, many alternative systems and models are being investigated, whose interrelationships are only partly understood. Improved collaboration between some of the foremost U.S. and French researchers in this area is likely to lead to important results in the classification and unification of those alternatives. Improved semantic models supporting the combination of parametric polymorphism and type inheritance would be of particular interest to the development of semantically more coherent object-oriented programming languages, a question of undoubted interest for software engineers. In a different area, the interaction between U.S. work on higher-order logic programming and French work on logic-based language definition systems promises to be very productive and lead to better prototyping environments for program-proving and language-definition systems.